Theorem nesym 3017

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  iunopeqop  5509  ord1eln01  8490  ord2eln012  8491  fiming  9470  wemapsolem  9522  nn01to3  12983  xrltlen  13189  sgnn  15157  isprm3  16766  lspsncv0  21307  uvcvv0  21977  fvmptnn04if  23043  chfacfisf  23048  chfacfisfcpmat  23049  trfbas  24038  fbunfip  24063  trfil2  24081  iundisj2  25745  nosupbnd2lem1  27916  noinfbnd2lem1  27931  elnns2  28571  pthdlem2lem  30153  fusgr2wsp2nb  30722  iundisj2f  32972  iundisj2fi  33179  cvmscld  35786  poimirlem25  38337  hlrelat5N  40216  redvmptabs  43162  cmpfiiin  43469  gneispace  44901  iblcncfioo  46733  fourierdlem82  46943  elprneb  47807  fzopredsuc  48102  iccpartiltu  48212