Definition df-ne 1587

Description: Define inequality.

Assertion

Ref	Expression
df-ne	|- (A =/= B <-> -. A = B)

Detailed syntax breakdown of Definition df-ne

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wne 1585	. 2 wff A =/= B
4	1, 2	wceq 956	. . 3 wff A = B
5	4	wn 2	. 2 wff -. A = B
6	3, 5	wb 146	1 wff (A =/= B <-> -. A = B)

This definition is referenced by:  nne 1589  neeq1 1590  neeq2 1591  necon3abii 1596  necon3bii 1598  necon3abid 1599  necon3bid 1601  necon3ad 1602  necon3bd 1603  necon3d 1604  necon3ai 1606  necon3bi 1607  necon1ai 1608  necon1bi 1609  necon1i 1610  necon2ai 1611  necon2bi 1612  necon2i 1613  necon2ad 1614  necon2bd 1615  necon1abii 1616  necon1bbii 1617  necon1abid 1618  necon1bbid 1619  necon2abid 1622  necon2bbid 1623  necon4ai 1624  necon4i 1625  necon4ad 1626  necon4bd 1627  necon4d 1628  necon4abid 1629  necon1ad 1631  necon1bd 1632  pm2.61ne 1633  pm2.61ine 1634  pm2.61dne 1635  neor 1638  neanior 1639  neorian 1640  nemtbir 1641  hbne 1644  dfpss2 2133  ne0i 2286  ne0f 2287  n0 2289  npss0 2309  disjne 2315  difsn 2464  difprsn 2465  eqsn 2474  snsssn 2478  opthpr 2485  iununi 2616  0inp0 2738  opprc1b 2796  ord0eln0 3023  nsuceq0 3053  orduniorsuc 3087  unizlim 3113  nn0suc 3154  findsg 3157  tfindsg 3162  fvprc 3721  fvopabn 3786  tz7.49 3959  oevn0 4154  2dom 4427  0sdomg 4466  mapdom2 4494  php 4513  fiint 4559  fiintOLD 4560  rankxplim2 4713  rankxplim3 4714  ac9s 4764  aceqkm 4781  zorn2lem4 4791  zorn2lem7 4794  brdom3 4801  card1 4833  ax1ne0 5280  axrrecex 5284  pre-axsup 5291  ine0 5434  ltlent 5522  pnfnemnf 5536  renepnft 5537  renemnft 5538  renfdisj 5539  xrltnrt 5541  pnfnltt 5546  nltmnft 5547  mul0or 5694  muln0bt 5697  eqneg 5804  recgt0i 5814  posex 5908  nnunb 6070  elnnz 6145  ioo0t 6368  nnwo 6458  infmssuzcl 6466  expnnvalt 6572  sumsqne0 6634  sq01t 6651  discrlem3 6658  sqrlem6 6678  inelr 6735  crulem 6736  crne0 6739  abssubne0t 6882  efseq1ex 7306  efne0t 7369  elcls 7704  islp2 7747  cnconst 7780  sncld 7787  dscmet 7918  bcthlem33 8031  vcoprne 8198  vcex 8199  nvex 8230  nvmul0or 8272  nmogtmnf 8433  pilem1 8671  sinhalfpilem 8679  efif1lem5 8734  hvmul0ort 8894  hvmulcant 8939  hvmulcan2t 8940  hiidge0t 8964  normgt0tOLD 8993  bcsALT 9046  norm1ex 9122  pjthlem11 9229  shne0 9371  h1datom 9504  nonbool 9596  eigorth 9763  nmopgtmnf 9795  unopbdt 9940  nmcoplb 9958  nmophm 9961  nmbdfnlb 9978  nmcfnlb 9987  nmopco 10028  strlem1 10177  strlem6 10183  hstrlem6 10191  large 10194  atssmat 10305  irredlem1 10317  irred 10321  sumdmdlem2 10346  uninqs 10441  fiiu 10453  fiiuOLD 10454  neiopne 10474  fiiu2 10488  fiiu2OLD 10489  topnem 10507  sfseqeq 10543  top2ind 10548  top2usne 10549  fipfil 10563  fipfil2 10564  fipfil2OLD 10565  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  dmse1 10623  iintlem1 10632

Copyright terms: Public domain