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 2116 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | |
2 | ax8 2116 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) | |
3 | 2 | equcoms 2028 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) |
4 | 1, 3 | impbid 215 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 |
This theorem is referenced by: elsb3 2118 cleljust 2119 ax12wdemo 2135 cleljustALT 2363 cleljustALT2 2364 dveel1 2460 axc14 2462 axsepgfromrep 5190 nalset 5206 zfpow 5259 dtru 5263 zfun 7524 tz7.48lem 8177 pssnn 8846 unxpdomlem1 8882 pssnnOLD 8895 zfinf 9254 aceq1 9731 aceq0 9732 aceq2 9733 dfac3 9735 dfac5lem2 9738 dfac5lem3 9739 dfac2a 9743 kmlem4 9767 zfac 10074 nd1 10201 axextnd 10205 axrepndlem1 10206 axrepndlem2 10207 axunndlem1 10209 axunnd 10210 axpowndlem2 10212 axpowndlem3 10213 axpowndlem4 10214 axregndlem1 10216 axregnd 10218 zfcndun 10229 zfcndpow 10230 zfcndinf 10232 zfcndac 10233 fpwwe2lem11 10255 axgroth3 10445 axgroth4 10446 nqereu 10543 mdetunilem9 21517 madugsum 21540 neiptopnei 22029 2ndc1stc 22348 nrmr0reg 22646 alexsubALTlem4 22947 xrsmopn 23709 itg2cn 24661 itgcn 24742 sqff1o 26064 dya2iocuni 31962 bnj849 32618 fineqvrep 32777 erdsze 32877 untsucf 33364 untangtr 33368 dfon2lem3 33480 dfon2lem6 33483 dfon2lem7 33484 dfon2 33487 axextdist 33494 distel 33498 neibastop2lem 34286 bj-elequ12 34597 bj-nfeel2 34775 bj-ru0 34868 prtlem5 36611 prtlem13 36619 prtlem16 36620 ax12el 36693 pw2f1ocnv 40562 aomclem8 40589 grumnud 41577 lcosslsp 45452 |
Copyright terms: Public domain | W3C validator |