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 211). (Contributed by BJ, 7-Jul-2018.) |
Ref | Expression |
---|---|
nesym | ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2617 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
2 | 1 | necon3abii 2828 | 1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 = wceq 1475 ≠ wne 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 df-ne 2782 |
This theorem is referenced by: 0neqopab 6596 fiming 8287 wemapsolem 8338 nn01to3 11657 xrltlen 11855 sgnn 13682 pwm1geoser 14439 isprm3 15234 lspsncv0 18967 uvcvv0 19948 fvmptnn04if 20473 chfacfisf 20478 chfacfisfcpmat 20479 trfbas 21458 fbunfip 21483 trfil2 21501 iundisj2 23124 2pthfrgra 26538 frgrawopreglem3 26573 usg2spot2nb 26592 iundisj2f 28785 iundisj2fi 28943 cvmscld 30509 poimirlem25 32604 hlrelat5N 33705 cmpfiiin 36278 gneispace 37452 iblcncfioo 38870 fourierdlem82 39081 elprneb 39939 fzopredsuc 39946 iccpartiltu 39960 pthdlem2lem 40973 fusgr2wsp2nb 41498 |
Copyright terms: Public domain | W3C validator |