| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elequ1 | Structured version Visualization version GIF version | ||
| Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.) |
| Ref | Expression |
|---|---|
| elequ1 | ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax8 2114 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | |
| 2 | ax8 2114 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) | |
| 3 | 2 | equcoms 2019 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) |
| 4 | 1, 3 | 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 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: elsb1 2116 cleljust 2117 elequ12 2126 ru0 2127 ax12wdemo 2135 cleljustALT 2367 cleljustALT2 2368 dveel1 2466 axc14 2468 sbralie 3358 unissb 4939 dftr2c 5262 axsepgfromrep 5294 nalset 5313 zfpow 5366 dtruALT2 5370 el 5442 dtruOLD 5446 zfun 7756 tz7.48lem 8481 coflton 8709 pssnn 9208 unxpdomlem1 9286 zfinf 9679 aceq1 10157 aceq0 10158 aceq2 10159 dfac3 10161 dfac5lem2 10164 dfac5lem3 10165 dfac2a 10170 kmlem4 10194 zfac 10500 nd1 10627 axextnd 10631 axrepndlem1 10632 axrepndlem2 10633 axunndlem1 10635 axunnd 10636 axpowndlem2 10638 axpowndlem3 10639 axpowndlem4 10640 axregndlem1 10642 axregnd 10644 zfcndun 10655 zfcndpow 10656 zfcndinf 10658 zfcndac 10659 fpwwe2lem11 10681 axgroth3 10871 axgroth4 10872 nqereu 10969 mdetunilem9 22626 madugsum 22649 neiptopnei 23140 2ndc1stc 23459 nrmr0reg 23757 alexsubALTlem4 24058 xrsmopn 24834 itg2cn 25798 itgcn 25880 sqff1o 27225 dya2iocuni 34285 bnj849 34939 axnulg 35106 fineqvrep 35109 erdsze 35207 untsucf 35710 untangtr 35714 dfon2lem3 35786 dfon2lem6 35789 dfon2lem7 35790 dfon2 35793 axextdist 35800 distel 35804 neibastop2lem 36361 bj-nfeel2 36855 prtlem5 38861 prtlem13 38869 prtlem16 38870 ax12el 38943 pw2f1ocnv 43049 aomclem8 43073 onsupmaxb 43251 grumnud 44305 dfnbgr6 47843 lcosslsp 48355 |
| Copyright terms: Public domain | W3C validator |