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 2387 axc15OLD 2439 dveeq2ALT 2471 sb4b 2495 sb4bOLD 2496 mojust 2617 mof 2643 eujust 2652 eujustALT 2653 eu6lem 2654 euf 2657 eleq1w 2895 disjxun 5056 axrep2 5185 dtru 5263 zfpair 5313 dfid3 5456 isso2i 5502 iotaval 6323 dff13f 7005 dfwe2 7484 aceq0 9533 zfac 9871 axpowndlem4 10011 zfcndac 10030 injresinj 13148 infpn2 16239 ramub1lem2 16353 fullestrcsetc 17391 fullsetcestrc 17406 symgextf1 18480 mplcoe1 20176 evlslem2 20222 mamulid 20980 mamurid 20981 mdetdiagid 21139 dscmet 23111 lgseisenlem2 25880 dchrisumlem3 25995 frgr2wwlk1 28036 bj-ssblem1 33885 bj-ssblem2 33886 bj-ax12 33888 bj-dtru 34037 wl-aleq 34657 wl-mo2df 34688 wl-eudf 34690 wl-euequf 34692 wl-mo2t 34693 dveeq2-o 35951 axc11n-16 35956 ax12eq 35959 ax12inda 35966 ax12v2-o 35967 fphpd 39293 iotavalb 40642 disjinfi 41334 eusnsn 43142 2reu8i 43193 2reuimp0 43194 ichexmpl1 43478 |
Copyright terms: Public domain | W3C validator |