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 212). (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesym | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2629 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3abii 2840 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 = wceq 1483 ≠ wne 2794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-ne 2795 |
This theorem is referenced by: 0neqopab 6698 fiming 8404 wemapsolem 8455 nn01to3 11781 xrltlen 11979 sgnn 13834 pwm1geoser 14600 isprm3 15396 lspsncv0 19146 uvcvv0 20129 fvmptnn04if 20654 chfacfisf 20659 chfacfisfcpmat 20660 trfbas 21648 fbunfip 21673 trfil2 21691 iundisj2 23317 pthdlem2lem 26663 fusgr2wsp2nb 27198 iundisj2f 29403 iundisj2fi 29556 cvmscld 31255 nosupbnd2lem1 31861 poimirlem25 33434 hlrelat5N 34687 cmpfiiin 37260 gneispace 38432 iblcncfioo 40194 fourierdlem82 40405 elprneb 41296 fzopredsuc 41333 iccpartiltu 41358 |
Copyright terms: Public domain | W3C validator |