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 1983 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | |
2 | ax8 1983 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) | |
3 | 2 | equcoms 1934 | . 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧)) |
4 | 1, 3 | 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 ax-8 1979 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: cleljust 1985 ax12wdemo 1999 cleljustALT 2173 cleljustALT2 2174 dveel1 2358 axc14 2360 elsb3 2422 axsep 4708 nalset 4723 zfpow 4770 zfun 6848 tz7.48lem 7423 unxpdomlem1 8049 pssnn 8063 zfinf 8419 aceq0 8824 dfac3 8827 dfac5lem2 8830 dfac5lem3 8831 dfac2a 8835 zfac 9165 nd1 9288 axextnd 9292 axrepndlem1 9293 axrepndlem2 9294 axunndlem1 9296 axunnd 9297 axpowndlem2 9299 axpowndlem3 9300 axpowndlem4 9301 axregndlem1 9303 axregnd 9305 zfcndun 9316 zfcndpow 9317 zfcndinf 9319 zfcndac 9320 fpwwe2lem12 9342 axgroth3 9532 axgroth4 9533 nqereu 9630 mdetunilem9 20245 madugsum 20268 neiptopnei 20746 2ndc1stc 21064 nrmr0reg 21362 alexsubALTlem4 21664 xrsmopn 22423 itg2cn 23336 itgcn 23415 sqff1o 24708 dya2iocuni 29672 bnj849 30249 erdsze 30438 untsucf 30841 untangtr 30845 dfon2lem3 30934 dfon2lem6 30937 dfon2lem7 30938 dfon2 30941 axextdist 30949 distel 30953 neibastop2lem 31525 bj-elequ12 31855 bj-axsep 31981 bj-nalset 31982 bj-zfpow 31983 bj-ru0 32124 prtlem5 33162 ax12el 33245 pw2f1ocnv 36622 aomclem8 36649 lcosslsp 42021 |
Copyright terms: Public domain | W3C validator |