Theorem nesym 3015

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 2770	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3abii 3005	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴)

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  iunopeqop  5498  ord1eln01  8532  ord2eln012  8533  fiming  9519  wemapsolem  9571  nn01to3  13095  xrltlen  13302  sgnn  15276  isprm3  16887  lspsncv0  21454  uvcvv0  22126  fvmptnn04if  23197  chfacfisf  23202  chfacfisfcpmat  23203  trfbas  24193  fbunfip  24218  trfil2  24236  iundisj2  25900  nosupbnd2lem1  28102  noinfbnd2lem1  28117  elnns2  28757  pthdlem2lem  30383  fusgr2wsp2nb  30965  iundisj2f  33256  iundisj2fi  33459  gdlopcfvlem  35971  cvmscld  36205  poimirlem25  38755  hlrelat5N  40650  redvmptabs  43604  cmpfiiin  43901  gneispace  45326  iblcncfioo  47193  fourierdlem82  47403  elprneb  48304  fzopredsuc  48599  iccpartiltu  48709