![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equequ2 | Structured version Visualization version GIF version |
Description: An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.) |
Ref | Expression |
---|---|
equequ2 | ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equtrr 2017 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
2 | equeuclr 2018 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
3 | 1, 2 | impbid 211 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 |
This theorem is referenced by: sbjust 2058 sbequ 2078 sb6 2080 equsb3r 2094 ax13lem2 2369 dveeq2ALT 2447 sb4b 2468 mojust 2527 mof 2551 eujust 2559 eujustALT 2560 eu6lem 2561 euf 2564 eleq1w 2808 mo2icl 3706 disjxun 5147 axrep2 5289 dtruALT2 5370 zfpair 5421 dtruOLD 5443 dfid3 5579 solin 5615 isso2i 5625 iotavalOLD 6523 dff13f 7266 dfwe2 7777 poxp2 8148 poxp3 8155 aceq0 10148 zfac 10490 axpowndlem4 10630 zfcndac 10649 injresinj 13794 infpn2 16890 ramub1lem2 17004 fullestrcsetc 18150 fullsetcestrc 18165 symgextf1 19393 mplcoe1 22002 evlslem2 22052 mamulid 22392 mamurid 22393 mdetdiagid 22551 dscmet 24530 lgseisenlem2 27359 dchrisumlem3 27474 frgr2wwlk1 30216 bj-ssblem1 36263 bj-ssblem2 36264 bj-ax12 36266 wl-aleq 37135 wl-mo2df 37170 wl-eudf 37172 wl-euequf 37174 wl-mo2t 37175 dveeq2-o 38537 axc11n-16 38542 ax12eq 38545 ax12inda 38552 ax12v2-o 38553 aks6d1c6lem3 41777 fsuppind 41960 eu6w 42238 fphpd 42380 iotavalb 44011 disjinfi 44706 eusnsn 46548 fcoresf1 46591 2reu8i 46633 2reuimp0 46634 ichexmpl1 46948 |
Copyright terms: Public domain | W3C validator |