![]() |
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 221). (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesym | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2735 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3abii 2984 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1534 ≠ wne 2937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-cleq 2720 df-ne 2938 |
This theorem is referenced by: 0nelopabOLD 5570 ord1eln01 8517 ord2eln012 8518 fiming 9522 wemapsolem 9574 nn01to3 12956 xrltlen 13158 sgnn 15074 isprm3 16654 lspsncv0 21034 uvcvv0 21724 fvmptnn04if 22764 chfacfisf 22769 chfacfisfcpmat 22770 trfbas 23761 fbunfip 23786 trfil2 23804 iundisj2 25491 nosupbnd2lem1 27661 noinfbnd2lem1 27676 elnns2 28222 pthdlem2lem 29594 fusgr2wsp2nb 30157 iundisj2f 32393 iundisj2fi 32578 cvmscld 34883 poimirlem25 37118 hlrelat5N 38874 cmpfiiin 42117 gneispace 43564 iblcncfioo 45366 fourierdlem82 45576 elprneb 46411 fzopredsuc 46703 iccpartiltu 46762 |
Copyright terms: Public domain | W3C validator |