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 1936 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
2 | equeuclr 1937 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
3 | 1, 2 | impbid 201 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: axc11nlemOLD2 1975 ax12vOLDOLD 2038 axc11nlemOLD 2146 ax13lem2 2284 axc15 2291 axc11nlemALT 2294 dveeq2ALT 2328 ax12v2OLD 2330 eujust 2460 eujustALT 2461 euequ1 2464 euf 2466 mo2 2467 disjxun 4581 axrep2 4701 dtru 4783 zfpair 4831 dfid3 4954 isso2i 4991 iotaval 5779 dff13f 6417 dfwe2 6873 aceq0 8824 zfac 9165 axpowndlem4 9301 zfcndac 9320 injresinj 12451 infpn2 15455 ramub1lem2 15569 fullestrcsetc 16614 fullsetcestrc 16629 symgextf1 17664 mplcoe1 19286 evlslem2 19333 mamulid 20066 mamurid 20067 mdetdiagid 20225 dscmet 22187 lgseisenlem2 24901 dchrisumlem3 24980 usgrasscusgra 26011 bj-ssbequ 31818 bj-ssblem1 31819 bj-ssblem2 31820 bj-ssb1a 31821 bj-ssb1 31822 bj-ssbcom3lem 31839 bj-axrep2 31977 bj-dtru 31985 bj-eleq1w 32040 bj-ax8 32080 wl-aleq 32501 wl-mo2df 32531 wl-eudf 32533 wl-euequ1f 32535 wl-mo2t 32536 dveeq2-o 33236 axc11n-16 33241 ax12eq 33244 ax12inda 33251 ax12v2-o 33252 fphpd 36398 iotavalb 37653 disjinfi 38375 |
Copyright terms: Public domain | W3C validator |