Definition df-ne 1579

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 1577	. 2 wff A =/= B
4	1, 2	wceq 953	. . 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 1581  neeq1 1582  neeq2 1583  necon3abii 1588  necon3bii 1590  necon3abid 1591  necon3bid 1593  necon3ad 1594  necon3bd 1595  necon3d 1596  necon3ai 1598  necon3bi 1599  necon1ai 1600  necon1bi 1601  necon1i 1602  necon2ai 1603  necon2bi 1604  necon2i 1605  necon2ad 1606  necon2bd 1607  necon1abii 1608  necon1bbii 1609  necon1abid 1610  necon1bbid 1611  necon2abid 1614  necon2bbid 1615  necon4ai 1616  necon4i 1617  necon4ad 1618  necon4bd 1619  necon4d 1620  necon4abid 1621  necon1ad 1623  necon1bd 1624  pm2.61ne 1625  pm2.61ine 1626  pm2.61dne 1627  neor 1630  neanior 1631  neorian 1632  nemtbir 1633  hbne 1636  dfpss2 2123  ne0i 2276  ne0f 2277  n0 2279  npss0 2299  disjne 2305  difsn 2455  difprsn 2456  eqsn 2465  snsssn 2469  opthpr 2476  iununi 2606  0inp0 2728  opprc1b 2786  ord0eln0 3013  nsuceq0 3043  orduniorsuc 3077  unizlim 3103  nn0suc 3144  findsg 3147  tfindsg 3152  fvprc 3706  fvopabn 3771  tz7.49 3944  oevn0 4138  2dom 4408  0sdomg 4446  mapdom2 4474  php 4493  fiint 4534  rankxplim2 4685  rankxplim3 4686  ac9s 4736  aceqkm 4753  zorn2lem4 4763  zorn2lem7 4766  brdom3 4773  card1 4805  ax1ne0 5252  axrrecex 5256  pre-axsup 5263  ine0 5406  ltnetOLD 5489  ltlent 5495  pnfnemnf 5509  renepnft 5510  renemnft 5511  renfdisj 5512  xrltnrt 5514  pnfnltt 5519  nltmnft 5520  mul0or 5663  muln0bt 5666  eqneg 5760  recgt0i 5770  posex 5856  nnunb 6017  elnnz 6092  ioo0t 6305  nnwo 6390  infmssuzcl 6398  expnnvalt 6504  sumsqne0 6565  sq01t 6582  discrlem3 6588  nn0opth 6596  sqrlem6 6608  inelr 6665  crulem 6666  crne0 6670  absgt0 6778  abssubne0t 6820  efseq1ex 7248  efne0t 7311  elcls 7646  islp2 7688  cnconst 7719  sncld 7726  dscmet 7856  bcthlem33 7965  vcoprne 8136  vcex 8137  nvex 8169  nvmul0or 8212  nmogtmnf 8365  pilem1 8590  sinhalfpilem 8598  efif1lem5 8649  hvmul0ort 8815  hvmulcant 8860  hvmulcan2t 8861  hiidge0t 8885  normgt0tOLD 8914  bcsALT 8967  norm1ex 9043  pjthlem11 9144  shne0 9286  spansneleqOLD 9410  h1datom 9421  nonbool 9513  eigorth 9680  nmopgtmnf 9712  unopbdt 9855  nmcoplb 9873  nmophm 9876  nmbdfnlb 9893  nmcfnlb 9902  nmopco 9942  strlem1 10087  large 10104  atssmat 10213  irredlem1 10225  irred 10229  sumdmdlem2 10253  uninqs 10342  fiiu 10350  neiopne 10369  fiiu2 10377  topnem 10394  fipfil 10438  fipfil2 10439  efilcp 10445  efilcp2 10450  cnfilca 10451  dmse1 10467  iintlem1 10476

Copyright terms: Public domain