| 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 2021 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
| 2 | equeuclr 2022 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
| 3 | 1, 2 | impbid 212 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: sbjust 2063 sbequ 2083 sb6 2085 equsb3r 2104 ax13lem2 2381 dveeq2ALT 2459 sb4b 2480 mojust 2539 mof 2563 eujust 2571 eujustALT 2572 eu6lem 2573 euf 2576 eleq1w 2824 mo2icl 3720 disjxun 5141 axrep2 5282 dtruALT2 5370 zfpair 5421 dtruOLD 5446 dfid3 5581 solin 5619 isso2i 5629 iotavalOLD 6535 dff13f 7276 dfwe2 7794 poxp2 8168 poxp3 8175 aceq0 10158 zfac 10500 axpowndlem4 10640 zfcndac 10659 injresinj 13827 infpn2 16951 ramub1lem2 17065 fullestrcsetc 18196 fullsetcestrc 18211 symgextf1 19439 mplcoe1 22055 evlslem2 22103 mamulid 22447 mamurid 22448 mdetdiagid 22606 dscmet 24585 lgseisenlem2 27420 dchrisumlem3 27535 frgr2wwlk1 30348 sbequbidv 36215 cbvsbdavw2 36256 bj-ssblem1 36655 bj-ssblem2 36656 bj-ax12 36658 wl-aleq 37536 wl-mo2df 37571 wl-eudf 37573 wl-euequf 37575 wl-mo2t 37576 dveeq2-o 38934 axc11n-16 38939 ax12eq 38942 ax12inda 38949 ax12v2-o 38950 aks6d1c6lem3 42173 fsuppind 42600 eu6w 42686 fphpd 42827 iotavalb 44449 disjinfi 45197 eusnsn 47038 fcoresf1 47081 2reu8i 47125 2reuimp0 47126 ichexmpl1 47456 |
| Copyright terms: Public domain | W3C validator |