|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nesym | Structured version Visualization version GIF version | ||
| Description: Characterization of inequality in terms of reversed equality (see bicom 222). (Contributed by BJ, 7-Jul-2018.) | 
| Ref | Expression | 
|---|---|
| nesym | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eqcom 2743 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
| 2 | 1 | necon3abii 2986 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ wb 206 = wceq 1539 ≠ wne 2939 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-ne 2940 | 
| This theorem is referenced by: ord1eln01 8535 ord2eln012 8536 fiming 9539 wemapsolem 9591 nn01to3 12984 xrltlen 13189 sgnn 15134 isprm3 16721 lspsncv0 21149 uvcvv0 21811 fvmptnn04if 22856 chfacfisf 22861 chfacfisfcpmat 22862 trfbas 23853 fbunfip 23878 trfil2 23896 iundisj2 25585 nosupbnd2lem1 27761 noinfbnd2lem1 27776 elnns2 28345 pthdlem2lem 29788 fusgr2wsp2nb 30354 iundisj2f 32604 iundisj2fi 32800 cvmscld 35279 poimirlem25 37653 hlrelat5N 39404 redvmptabs 42395 cmpfiiin 42713 gneispace 44152 iblcncfioo 45998 fourierdlem82 46208 elprneb 47046 fzopredsuc 47340 iccpartiltu 47414 | 
| Copyright terms: Public domain | W3C validator |