![]() |
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 2113 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | |
2 | ax9 2113 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) | |
3 | 2 | equcoms 2016 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) |
4 | 1, 3 | impbid 211 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 |
This theorem is referenced by: elequ2g 2115 elsb2 2116 ax12wdemo 2124 dveel2 2457 axextg 2701 axextmo 2703 eleq2w 2813 nfcvf 2929 unissb 4942 dftr2c 5268 axrep1 5286 axreplem 5287 axrep4 5290 axsepg 5300 bm1.3ii 5302 nalset 5313 fv3 6915 zfun 7741 tz7.48lem 8462 coflton 8692 aceq1 10141 aceq0 10142 aceq2 10143 dfac2a 10153 kmlem4 10177 axdc3lem2 10475 zfac 10484 nd2 10612 nd3 10613 axrepndlem2 10617 axunndlem1 10619 axunnd 10620 axpowndlem2 10622 axpowndlem3 10623 axpowndlem4 10624 axpownd 10625 axregndlem2 10627 axregnd 10628 axinfndlem1 10629 axacndlem5 10635 zfcndrep 10638 zfcndun 10639 zfcndac 10643 axgroth4 10856 nqereu 10953 mdetunilem9 22535 neiptopnei 23049 2ndc1stc 23368 restlly 23400 kqt0lem 23653 regr1lem2 23657 nrmr0reg 23666 hauspwpwf1 23904 dya2iocuni 33903 erdsze 34812 untsucf 35304 untangtr 35308 dfon2lem3 35381 dfon2lem6 35384 dfon2lem7 35385 dfon2lem8 35386 dfon2 35388 axextbdist 35396 distel 35399 axextndbi 35400 fness 35833 fneref 35834 bj-elequ12 36155 bj-axc14nf 36332 bj-bm1.3ii 36543 matunitlindflem1 37089 prtlem13 38340 prtlem15 38347 prtlem17 38348 dveel2ALT 38411 ax12el 38414 aomclem8 42485 unielss 42646 elintima 43083 mnuprdlem3 43711 ismnushort 43738 axc11next 43843 setcthin 48061 |
Copyright terms: Public domain | W3C validator |