Theorem nesym 3012

Description: Characterization of inequality in terms of reversed equality (see bicom 225). (Contributed by BJ, 7-Jul-2018.)

Assertion

Ref	Expression
nesym	⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

Proof of Theorem nesym

Step	Hyp	Ref	Expression
1		eqcom 2768	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3abii 3002	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  iunopeqop  5494  ord1eln01  8488  ord2eln012  8489  fiming  9476  wemapsolem  9528  nn01to3  13049  xrltlen  13256  sgnn  15227  isprm3  16838  lspsncv0  21404  uvcvv0  22076  fvmptnn04if  23147  chfacfisf  23152  chfacfisfcpmat  23153  trfbas  24143  fbunfip  24168  trfil2  24186  iundisj2  25850  nosupbnd2lem1  28054  noinfbnd2lem1  28069  elnns2  28709  pthdlem2lem  30335  fusgr2wsp2nb  30917  iundisj2f  33166  iundisj2fi  33371  cvmscld  36007  poimirlem25  38531  hlrelat5N  40426  redvmptabs  43379  cmpfiiin  43661  gneispace  45093  iblcncfioo  46932  fourierdlem82  47142  elprneb  48043  fzopredsuc  48338  iccpartiltu  48448