| 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 2122 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | |
| 2 | ax9 2122 | . . 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-9 2118 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: elequ2g 2124 elsb2 2125 elequ12 2126 ax12wdemo 2135 dveel2 2467 axextg 2710 axextmo 2712 eleq2w 2825 nfcvf 2932 unissb 4939 dftr2c 5262 axrep1 5280 axreplem 5281 axrep4OLD 5286 axsepg 5297 bm1.3iiOLD 5302 nalset 5313 fv3 6924 zfun 7756 tz7.48lem 8481 coflton 8709 aceq1 10157 aceq0 10158 aceq2 10159 dfac2a 10170 kmlem4 10194 axdc3lem2 10491 zfac 10500 nd2 10628 nd3 10629 axrepndlem2 10633 axunndlem1 10635 axunnd 10636 axpowndlem2 10638 axpowndlem3 10639 axpowndlem4 10640 axpownd 10641 axregndlem2 10643 axregnd 10644 axinfndlem1 10645 axacndlem5 10651 zfcndrep 10654 zfcndun 10655 zfcndac 10659 axgroth4 10872 nqereu 10969 mdetunilem9 22626 neiptopnei 23140 2ndc1stc 23459 restlly 23491 kqt0lem 23744 regr1lem2 23748 nrmr0reg 23757 hauspwpwf1 23995 dya2iocuni 34285 axsepg2 35096 axsepg2ALT 35097 axnulg 35106 erdsze 35207 untsucf 35710 untangtr 35714 dfon2lem3 35786 dfon2lem6 35789 dfon2lem7 35790 dfon2lem8 35791 dfon2 35793 axextbdist 35801 distel 35804 axextndbi 35805 fness 36350 fneref 36351 bj-axc14nf 36856 bj-bm1.3ii 37065 matunitlindflem1 37623 prtlem13 38869 prtlem15 38876 prtlem17 38877 dveel2ALT 38940 ax12el 38943 aomclem8 43073 unielss 43230 elintima 43666 mnuprdlem3 44293 ismnushort 44320 axc11next 44425 setcthin 49112 |
| Copyright terms: Public domain | W3C validator |