![]() |
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 1980 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
2 | equeuclr 1981 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
3 | 1, 2 | impbid 204 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 |
This theorem is referenced by: sbjust 2015 sbequ 2036 sb6 2038 equsb3r 2047 ax13lem2 2306 axc15OLD 2359 dveeq2ALT 2391 sb4b 2425 mojust 2550 mof 2580 mofOLD 2581 eujust 2591 eujustALT 2592 eu6lem 2593 eu6OLDOLD 2597 euf 2598 eufOLD 2599 euequOLD 2621 eleq1w 2850 disjxun 4932 axrep2 5056 dtru 5128 zfpair 5182 dfid3 5317 isso2i 5364 iotaval 6168 dff13f 6845 dfwe2 7318 aceq0 9344 zfac 9686 axpowndlem4 9826 zfcndac 9845 injresinj 12979 infpn2 16111 ramub1lem2 16225 fullestrcsetc 17271 fullsetcestrc 17286 symgextf1 18322 mplcoe1 19971 evlslem2 20017 mamulid 20769 mamurid 20770 mdetdiagid 20928 dscmet 22900 lgseisenlem2 25669 dchrisumlem3 25784 frgr2wwlk1 27878 bj-ssblem1 33535 bj-ssblem2 33536 bj-ax12 33538 bj-axrep2 33659 bj-dtru 33665 wl-aleq 34257 wl-mo2df 34287 wl-eudf 34289 wl-euequf 34291 wl-mo2t 34292 dveeq2-o 35554 axc11n-16 35559 ax12eq 35562 ax12inda 35569 ax12v2-o 35570 fphpd 38850 iotavalb 40220 disjinfi 40915 eusnsn 42701 2reu8i 42753 2reuimp0 42754 ichexmpl1 43034 |
Copyright terms: Public domain | W3C validator |