Definition df-ne 1584

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 1582	. 2 wff A ≠ B
4	1, 2	wceq 954	. . 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 1586  neeq1 1587  neeq2 1588  necon3abii 1593  necon3bii 1595  necon3abid 1596  necon3bid 1598  necon3ad 1599  necon3bd 1600  necon3d 1601  necon3ai 1603  necon3bi 1604  necon1ai 1605  necon1bi 1606  necon1i 1607  necon2ai 1608  necon2bi 1609  necon2i 1610  necon2ad 1611  necon2bd 1612  necon1abii 1613  necon1bbii 1614  necon1abid 1615  necon1bbid 1616  necon2abid 1619  necon2bbid 1620  necon4ai 1621  necon4i 1622  necon4ad 1623  necon4bd 1624  necon4d 1625  necon4abid 1626  necon1ad 1628  necon1bd 1629  pm2.61ne 1630  pm2.61ine 1631  pm2.61dne 1632  neor 1635  neanior 1636  neorian 1637  nemtbir 1638  hbne 1641  dfpss2 2129  ne0i 2282  ne0f 2283  n0 2285  npss0 2305  disjne 2311  difsn 2460  difprsn 2461  eqsn 2470  snsssn 2474  opthpr 2481  iununi 2611  0inp0 2733  opprc1b 2791  ord0eln0 3018  nsuceq0 3048  orduniorsuc 3082  unizlim 3108  nn0suc 3149  findsg 3152  tfindsg 3157  fvprc 3712  fvopabn 3777  tz7.49 3950  oevn0 4144  2dom 4414  0sdomg 4452  mapdom2 4480  php 4499  fiint 4540  rankxplim2 4693  rankxplim3 4694  ac9s 4744  aceqkm 4761  zorn2lem4 4771  zorn2lem7 4774  brdom3 4781  card1 4813  ax1ne0 5260  axrrecex 5264  pre-axsup 5271  ine0 5414  ltnetOLD 5497  ltlent 5503  pnfnemnf 5517  renepnft 5518  renemnft 5519  renfdisj 5520  xrltnrt 5522  pnfnltt 5527  nltmnft 5528  mul0or 5671  muln0bt 5674  eqneg 5768  recgt0i 5778  posex 5864  nnunb 6025  elnnz 6100  ioo0t 6313  nnwo 6398  infmssuzcl 6406  expnnvalt 6512  sumsqne0 6573  sq01t 6590  discrlem3 6596  nn0opth 6604  sqrlem6 6616  inelr 6673  crulem 6674  crne0 6678  absgt0 6786  abssubne0t 6828  efseq1ex 7256  efne0t 7319  elcls 7654  islp2 7697  cnconst 7730  sncld 7737  dscmet 7870  bcthlem33 7981  vcoprne 8150  vcex 8151  nvex 8182  nvmul0or 8224  nmogtmnf 8378  pilem1 8609  sinhalfpilem 8617  efif1lem5 8668  hvmul0ort 8833  hvmulcant 8878  hvmulcan2t 8879  hiidge0t 8903  normgt0tOLD 8932  bcsALT 8985  norm1ex 9061  pjthlem11 9167  shne0 9309  spansneleqOLD 9433  h1datom 9444  nonbool 9536  eigorth 9703  nmopgtmnf 9735  unopbdt 9878  nmcoplb 9896  nmophm 9899  nmbdfnlb 9916  nmcfnlb 9925  nmopco 9966  strlem1 10115  large 10132  atssmat 10242  irredlem1 10254  irred 10258  sumdmdlem2 10282  uninqs 10378  fiiu 10386  neiopne 10405  fiiu2 10413  topnem 10430  fipfil 10474  fipfil2 10475  efilcp 10481  efilcp2 10486  cnfilca 10487  dmse1 10503  iintlem1 10512

Copyright terms: Public domain