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 2020 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
2 | equeuclr 2021 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
3 | 1, 2 | impbid 213 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 |
This theorem is referenced by: sbjust 2059 sbequ 2081 sb6 2084 equsb3r 2101 ax13lem2 2385 axc15OLD 2436 dveeq2ALT 2468 sb4b 2492 sb4bOLD 2493 mojust 2614 mof 2640 eujust 2649 eujustALT 2650 eu6lem 2651 euf 2654 eleq1w 2892 disjxun 5055 axrep2 5184 dtru 5262 zfpair 5312 dfid3 5455 isso2i 5501 iotaval 6322 dff13f 7005 dfwe2 7485 aceq0 9532 zfac 9870 axpowndlem4 10010 zfcndac 10029 injresinj 13146 infpn2 16237 ramub1lem2 16351 fullestrcsetc 17389 fullsetcestrc 17404 symgextf1 18478 mplcoe1 20174 evlslem2 20220 mamulid 20978 mamurid 20979 mdetdiagid 21137 dscmet 23109 lgseisenlem2 25879 dchrisumlem3 25994 frgr2wwlk1 28035 bj-ssblem1 33884 bj-ssblem2 33885 bj-ax12 33887 bj-dtru 34036 wl-aleq 34656 wl-mo2df 34687 wl-eudf 34689 wl-euequf 34691 wl-mo2t 34692 dveeq2-o 35949 axc11n-16 35954 ax12eq 35957 ax12inda 35964 ax12v2-o 35965 fphpd 39291 iotavalb 40639 disjinfi 41330 eusnsn 43138 2reu8i 43189 2reuimp0 43190 ichexmpl1 43508 |
Copyright terms: Public domain | W3C validator |