Definition df-ne 2297

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 2295	. 2 wff A =/= B
4	1, 2	wceq 1615	. . 3 wff A = B
5	4	wn 2	. 2 wff -. A = B
6	3, 5	wb 231	1 wff (A =/= B <-> -. A = B)

This definition is referenced by:  nne 2299  exmidne 2300  nonconne 2301  neeq1 2302  neeq2 2303  necon3abii 2324  necon3bii 2326  necon3abid 2327  necon3bid 2329  necon3d 2332  necon1ai 2336  necon1i 2338  necon2bi 2340  necon2i 2341  necon2bd 2343  necon2d 2344  necon1abii 2345  necon1bbii 2346  necon1abid 2347  necon1bbid 2348  necon2abid 2351  necon2bbid 2352  necon4abid 2358  necon1ad 2361  neor 2375  neanior 2376  neorian 2377  nemtbir 2378  hbne 2383  hbned 2698  dfpss2 2951  ne0i 3120  n0f 3122  neq0 3124  eqsn 3364  snsssn 3368  opthpr 3375  unissint 3455  iununi 3533  0inp0 3675  opprc1b 3737  ord0eln0 3896  nsuceq0 3923  unizlim 3958  orduniorsuc 4083  dflim3 4100  tfindsg 4112  nn0suc 4142  findsg 4145  onnev 4234  xpcan 4492  xpcan2 4494  fvprc 4801  fvopabn 4874  tz7.49OLD 5373  tz7.49 5375  oevn0 5405  0nelqs 5561  2dom 5690  ac6sfilem3 5717  0sdomg 5738  sdomdif 5758  pwne 5764  2pwne 5765  mapdom2 5823  php 5843  1sdom 5859  fimax 5890  fimax2g 5893  fiint 5916  ordtypelem4 5962  card2on 5970  rankxplim2 6125  rankxplim3 6126  onfrALTlem5 6141  onfrALTlem3 6143  cardval3 6169  carden2a 6186  card1 6188  axcc2lem 6360  ac9 6399  ac9s 6410  aceqkm 6427  zorn2lem4 6438  zorn2lem7 6441  brdom3 6451  card1OLD 6472  ax1ne0 6875  axrrecex 6878  axpre-sup 6884  1re 6941  ltlen 6983  xrltnr 7002  pnfnlt 7007  nltmnf 7008  mul02lem1 7073  ine0 7178  mul0ori 7316  eqnegi 7415  recgt0ii 7425  posexi 7526  nnunb 7731  elnnz 7807  ioo0 7993  uzm1 8066  fzprval 8164  fztpval 8165  expnnval 8315  sumsqne0i 8379  sq01 8397  discrlem3 8408  sqrlem6 8428  inelr 8485  crulem 8486  crne0i 8489  abssubne0 8634  efseq1ex 9084  efne0 9147  egt2OLD 9173  elt3OLD 9174  egt2lt3 9175  dvdsle 9422  divalglem8 9433  ndvdssub 9440  gcdn0gt0 9458  gcd0id 9459  nn0seqcvgd 9469  algcvgblem 9476  eucalglt 9484  mulgcdlem2 9488  isprm2lem 9504  isprm2 9505  isprm3 9506  isprm4 9507  4nprm 9512  coprm 9513  divrngid 9681  pleval2 9710  elcls 9994  opnnei 10025  islp2 10039  cnconst 10073  sncld 10080  dscmet 10212  bcthlem33 10327  gxpval 10403  gxnval 10404  vcoprne 10551  vcex 10552  nvex 10583  nvmul0or 10625  nmogtmnf 10793  pilem1 11047  sinhalfpilem 11055  efif1lem5 11115  fiuni 11212  fiiu2 11213  fipfil 11267  fipfil2 11268  fbunfip 11278  extbas1 11287  hausfillim 11299  ismgm 11363  hvmul0or 11522  hvmulcan 11567  hvmulcan2 11568  hiidge0 11592  bcsiALT 11673  norm1exi 11747  pjthlem11 11854  shne0i 11996  nonbooli 12221  nmopgtmnf 12422  unopbd 12567  nmcoplbi 12585  lnopconi 12590  nmbdfnlbi 12605  nmcfnlbi 12614  nmopcoi 12655  strlem1 12811  strlem6 12817  hstrlem6 12825  largei 12828  atssma 12939  irredlem1 12951  irredi 12955  mdsymlem5 12968  sumdmdlem2 12980  bnj1120 13859  bnj1524 14106  bnj1540 14116  bnj71 14135  bnj1253 14399  ordsucuniel 14742  wfrlem16 14872  sltval2 14909  nosgnn0 14911  nosgnn0i 14912  sltintdifex 14916  sltres 14917  axsltsolem1 14921  axdenselem3 14937  axdenselem4 14938  axdenselem5 14939  axdenselem7 14941  axfelem9 14954  axfelem10 14955  axfelem15 14960  axfelem18 14963  axfelem22 14967  uninqs 15309  fiiu 15313  neiopne 15325  vxveqv 15328  fldsqcp2 15349  repcpwti 15503  cbcpcp 15504  topnem 15872  top2ind 15915  top2usne 15916  efilcp 15949  efilcp2 15953  cnfilca 15954  elfilnemp 15962  cntrsetlem 16052  dmse1 16054  iintlem1 16063  miminf 16083  mreal 16084  cptarc 16313  elicc3 16447  elfiun 16454  ordtypelem4OLD 16463  opnneiOLD 16502  compfipin0lem 16520  compfipin0 16521  dfcon2 16527  reconnlem1 16531  reconnlem4 16534  ivthALT 16539  topmtcl 16610  topjoin 16612  fbasfip 16641  supfil 16645  uffinfix 16662  fimaxOLD 16831  fimax2gOLD 16854  divexp 16864  uzm1OLD 16869  fzm1 16881  fdc 16897  heiborlem11 17050  heiborlem13 17052  heiborlem14 17053  heiborlem40 17079  rrndm 17100  rrntotbnd 17107  maxidln0 17278  prtlem90 17331  0nelqs2 17354  pm13.196a 17463  elnev 17489  compne 17502  en3lpVD 17764  onfrALTlem5VD 17804  onfrALTlem3VD 17806  cvrval2 17927  cvrnbtwn2 17928  cvrnbtwn3 17929  cvlsupr3 18004  hlrelat5 18061  cvrat4 18104  2atm0atz 18226  2atmatzOLD 18228  dalawlem13 18587  lhpocnle 18696  isltrn2 18754  trlatz 18842  trlval3 18855  cdleme18c 18960  cdleme22b 19009  cdlemg0or 19320  cdlemg17b 19340  cdlemg17i 19347

Copyright terms: Public domain