Definition df-ne 1630

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 1628	. 2 wff A ≠ B
4	1, 2	wceq 992	. . 3 wff A = B
5	4	wn 2	. 2 wff ¬ A = B
6	3, 5	wb 144	1 wff (A ≠ B ↔ ¬ A = B)

This definition is referenced by:  nne 1632  neeq1 1633  neeq2 1634  necon3abii 1639  necon3bii 1641  necon3abid 1642  necon3bid 1644  necon3ad 1645  necon3bd 1646  necon3d 1647  necon3ai 1649  necon3bi 1650  necon1ai 1651  necon1bi 1652  necon1i 1653  necon2ai 1654  necon2bi 1655  necon2i 1656  necon2ad 1657  necon2bd 1658  necon2d 1659  necon1abii 1660  necon1bbii 1661  necon1abid 1662  necon1bbid 1663  necon2abid 1666  necon2bbid 1667  necon4ai 1668  necon4i 1669  necon4ad 1670  necon4bd 1671  necon4d 1672  necon4abid 1673  necon1ad 1675  necon1bd 1676  necon1d 1677  pm2.61ne 1679  pm2.61ine 1680  pm2.61dne 1681  neor 1684  neanior 1685  neorian 1686  nemtbir 1687  hbne 1690  dfpss2 2185  ne0i 2338  ne0f 2340  neq0 2342  npss0 2362  disjne 2368  difsn 2528  difprsn 2529  eqsn 2539  snsssn 2543  opthpr 2550  iununi 2686  0inp0 2812  opprc1b 2872  ord0eln0 3027  nsuceq0 3053  unizlim 3086  orduniorsuc 3184  tfindsg 3213  nn0suc 3242  findsg 3245  fvprc 3832  fvopabn 3897  tz7.49 4260  oevn0 4290  0nelqs 4439  2dom 4568  ac6sfilem3 4590  0sdomg 4611  pwne 4633  2pwne 4634  mapdom2 4641  php 4660  fiint 4703  rankxplim2 4859  rankxplim3 4860  ac9s 4910  aceqkm 4927  zorn2lem4 4937  zorn2lem7 4940  brdom3 4947  card1 4981  ax1ne0 5434  axrrecex 5438  pre-axsup 5445  ine0 5588  ltlen 5676  renepnf 5691  renemnf 5692  renfdisj 5693  xrltnr 5695  pnfnlt 5700  nltmnf 5701  mul0ori 5846  muln0b 5849  eqnegi 5944  recgt0ii 5954  posexi 6053  nnunb 6238  elnnz 6313  ioo0 6494  nnwo 6585  infmssuzcl 6594  expnnval 6767  sumsqne0i 6831  sq01 6848  discrlem3 6859  sqrlem6 6879  inelr 6936  crulem 6937  crne0i 6940  abssubne0 7085  efseq1ex 7511  efne0 7574  egt2OLD 7600  elt3OLD 7601  egt2lt3 7602  elcls 7914  islp2 7957  cnconst 7990  sncld 7997  dscmet 8129  bcthlem33 8242  gxpval 8315  gxnval 8316  vcoprne 8445  vcex 8446  nvex 8477  nvmul0or 8519  nmogtmnf 8687  pilem1 8938  sinhalfpilem 8946  efif1lem5 9006  hvmul0or 9169  hvmulcan 9214  hvmulcanOLD 9215  hvmulcan2 9216  hiidge0 9240  normgt0OLD 9269  bcsiALT 9322  norm1exi 9398  pjthlem11 9505  shne0i 9647  nonbooli 9874  nmopgtmnf 10075  unopbd 10219  nmcoplbi 10237  nmophmi 10240  nmbdfnlbi 10257  nmcfnlbi 10266  nmopcoi 10307  strlem1 10458  strlem6 10464  hstrlem6 10472  largei 10475  atssma 10587  irredlem1 10599  irredi 10603  sumdmdlem2 10628  uninqs 10730  fiiu 10738  neiopne 10757  vxveqv 10761  fldsqcp2 10780  fiiu2 10852  ismgm 10897  topnem 11008  top2ind 11050  top2usne 11051  fipfil 11076  fipfil2 11077  efilcp 11083  efilcp2 11087  cnfilca 11088  dmse1 11146  iintlem1 11155  elicc3 11410  fiuni 11420  elfiun 11421  ordtypelem4 11430  opnnei 11469  compfipin0lem 11492  compfipin0 11493  dfcon2 11501  reconnlem1 11507  reconnlem4 11510  ivthALT 11515  topmtcl 11586  topjoin 11588  fbasfip 11627  fbunfip 11631  extbas1 11641  supfil 11645  uffinfix 11662  hausfillim 11685  fimax 11837  divexp 11859  uzm1 11862  fzm1 11867  heiborlem11 12021  heiborlem13 12023  heiborlem14 12024  heiborlem40 12050  rrndm 12071  rrntotbnd 12078

Copyright terms: Public domain