Definition df-ne 2019

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

This definition is referenced by:  nne 2021  exmidne 2022  nonconne 2023  neeq1 2024  neeq2 2025  necon3abii 2030  necon3bii 2032  necon3abid 2033  necon3bid 2035  necon3bidOLD 2036  necon3adOLD 2038  necon3bdOLD 2040  necon3d 2041  necon3aiOLD 2044  necon3biOLD 2046  necon1ai 2047  necon1biOLD 2049  necon1i 2050  necon2aiOLD 2052  necon2bi 2053  necon2i 2054  necon2adOLD 2056  necon2bd 2057  necon2d 2058  necon1abii 2059  necon1bbii 2060  necon1abid 2061  necon1bbid 2062  necon2abid 2065  necon2bbid 2066  necon4aiOLD 2068  necon4iOLD 2070  necon4adOLD 2072  necon4bdOLD 2074  necon4dOLD 2076  necon4abid 2077  necon1ad 2079  necon1bdOLD 2081  necon1dOLD 2083  pm2.61neOLD 2088  pm2.61ineOLD 2090  pm2.61dneOLD 2092  neor 2096  neanior 2097  neorian 2098  nemtbir 2099  hbne 2103  dfpss2 2694  ne0i 2881  ne0f 2883  neq0 2885  npss0OLD 2912  disjneOLD 2920  difsnOLD 3126  difprsnOLD 3128  eqsn 3143  snsssn 3148  opthpr 3156  unissint 3241  unissintOLD 3242  iununi 3331  iununiOLD 3332  0inp0 3475  opprc1b 3542  ord0eln0 3717  nsuceq0 3749  unizlim 3786  orduniorsuc 3909  dflim3 3930  tfindsg 3944  nn0suc 3976  findsg 3980  xpcan 4348  xpcan2 4350  fvprc 4678  fvopabn 4749  tz7.49 5168  oevn0 5199  0nelqs 5357  2dom 5486  ac6sfilem3 5508  0sdomg 5529  pwne 5552  2pwne 5553  mapdom2 5588  php 5607  fiint 5650  ordtypelem4 5687  rankxplim2 5824  rankxplim3 5825  ac9s 5926  aceqkm 5943  zorn2lem4 5953  zorn2lem7 5956  brdom3 5963  card1 5983  ax1ne0 6433  axrrecex 6437  pre-axsup 6444  ine0 6597  ltlen 6692  renepnfOLD 6709  renemnfOLD 6711  renfdisjOLD 6713  xrltnr 6716  pnfnlt 6721  nltmnf 6722  mul0ori 6882  mulne0bOLD 6886  eqnegi 6982  recgt0ii 6992  posexi 7091  nnunb 7279  elnnz 7354  ioo0 7535  nnwo 7627  infmssuzcl 7636  fzprval 7687  fztpval 7688  expnnval 7815  sumsqne0i 7879  sq01 7897  discrlem3 7908  sqrlem6 7928  inelr 7985  crulem 7986  crne0i 7989  abssubne0 8134  efseq1ex 8568  efne0 8631  egt2OLD 8657  elt3OLD 8658  egt2lt3 8659  elcls 8980  islp2 9023  cnconst 9057  sncld 9064  dscmet 9196  bcthlem33 9309  gxpval 9382  gxnval 9383  vcoprne 9530  vcex 9531  nvex 9562  nvmul0or 9604  nmogtmnf 9772  pilem1 10020  sinhalfpilem 10028  efif1lem5 10088  fiuni 10219  fiiu2 10220  fipfil 10271  fipfil2 10272  fbunfip 10282  extbas1 10291  hausfillim 10303  ismgm 10367  hvmul0or 10526  hvmulcan 10571  hvmulcanOLD 10572  hvmulcan2 10573  hiidge0 10597  normgt0OLD 10626  bcsiALT 10679  norm1exi 10755  pjthlem11 10862  shne0i 11004  nonbooli 11231  nmopgtmnf 11432  unopbd 11577  nmcoplbi 11595  nmophmi 11598  nmbdfnlbi 11615  nmcfnlbi 11624  nmopcoi 11665  strlem1 11822  strlem6 11828  hstrlem6 11836  largei 11839  atssma 11950  irredlem1 11962  irredi 11966  mdsymlem5 11979  sumdmdlem2 11991  bnj14OLD 12382  bnj1120 12930  bnj1524 13177  bnj1540 13187  bnj71 13206  bnj1253 13470  nn0seqcvgd 13659  dvdsle 13693  divalglem8 13703  ndvdssub 13710  gcdn0gt0 13728  gcd0id 13729  algcvgblem 13745  eucalglt 13753  mulgcdlem2 13757  isprm2lem 13774  isprm2 13775  isprm3 13776  coprm 13782  ordsucuniel 13863  wfrlem16 13972  sltval2 13997  nosgnn0 13999  nosgnn0i 14000  sltintdifex 14004  axsltsolem1 14006  axdenselem4 14022  axdenselem5 14023  axdenselem7 14025  axfelem8 14038  axfelem9 14039  axfelem11 14041  axfelem12 14042  axfelem15 14045  uninqs 14340  fiiu 14344  neiopne 14354  vxveqv 14357  fldsqcp2 14378  repcpwti 14503  cbcpcp 14504  topnem 14858  top2ind 14897  top2usne 14898  efilcp 14922  efilcp2 14926  cnfilca 14927  elfilnemp 14935  cntrsetlem 14999  dmse1 15001  iintlem1 15010  miminf 15028  mreal 15029  cptarc 15242  elicc3 15362  elfiun 15369  ordtypelem4OLD 15378  opnnei 15417  compfipin0lem 15435  compfipin0 15436  dfcon2 15442  reconnlem1 15446  reconnlem4 15449  ivthALT 15454  topmtcl 15525  topjoin 15527  fbasfip 15556  supfil 15560  uffinfix 15577  fimax 15746  fimax2g 15769  divexp 15779  uzm1 15784  fzm1 15796  fdc 15812  heiborlem11 15965  heiborlem13 15967  heiborlem14 15968  heiborlem40 15994  rrndm 16015  rrntotbnd 16022  maxidln0 16193  prtlem90 16246  0nelqs2 16269  pm13.196a 16378  elnev 16404  compne 16417  en3lpVD 16669  stb2val2 16736  stb3val2 16740  stb3val3 16741  stb2xpl 16742  stb3xpl 16743  pleval2 16785  cvrval2 16991  cvrnbtwn2 16992  cvrnbtwn3 16993  hlrelat5 17050  cvrat4 17076  divrngidNEW 17166

Copyright terms: Public domain