![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elequ2 | Structured version Visualization version GIF version |
Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
elequ2 | ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax9 2063 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | |
2 | ax9 2063 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) | |
3 | 2 | equcoms 1977 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) |
4 | 1, 3 | 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 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 |
This theorem is referenced by: elequ2g 2065 ax12wdemo 2073 dveel2 2399 elsb4 2409 axext3 2752 axext3ALT 2753 axextmo 2755 eleq2w 2849 nfcvf 2958 axrep1 5050 axreplem 5051 axrep4 5054 axsep2 5061 bm1.3ii 5063 nalset 5074 fv3 6517 zfun 7280 tz7.48lem 7880 aceq1 9337 aceq0 9338 aceq2 9339 dfac2a 9349 kmlem4 9373 axdc3lem2 9671 zfac 9680 nd2 9808 nd3 9809 axrepndlem2 9813 axunndlem1 9815 axunnd 9816 axpowndlem2 9818 axpowndlem3 9819 axpowndlem4 9820 axpownd 9821 axregndlem2 9823 axregnd 9824 axinfndlem1 9825 axacndlem5 9831 zfcndrep 9834 zfcndun 9835 zfcndac 9839 axgroth4 10052 nqereu 10149 mdetunilem9 20933 neiptopnei 21444 2ndc1stc 21763 restlly 21795 kqt0lem 22048 regr1lem2 22052 nrmr0reg 22061 hauspwpwf1 22299 dya2iocuni 31192 erdsze 32040 untsucf 32462 untangtr 32466 dfon2lem3 32556 dfon2lem6 32559 dfon2lem7 32560 dfon2lem8 32561 dfon2 32563 axext4dist 32572 distel 32575 axextndbi 32576 fness 33224 fneref 33225 bj-elequ12 33528 bj-axext3 33608 bj-axrep1 33624 bj-axrep2 33625 bj-axrep3 33626 bj-axrep4 33627 bj-axc14nf 33676 bj-axsep2 33743 bj-bm1.3ii 33872 matunitlindflem1 34335 prtlem13 35455 prtlem15 35462 prtlem17 35463 dveel2ALT 35526 ax12el 35529 aomclem8 39063 elintima 39367 mnuprdlem3 39991 axc11next 40161 |
Copyright terms: Public domain | W3C validator |