![]() |
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 2105 | . 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | |
2 | ax8 2105 | . . 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-8 2101 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 |
This theorem is referenced by: elsb1 2107 cleljust 2108 ax12wdemo 2124 cleljustALT 2357 cleljustALT2 2358 dveel1 2456 axc14 2458 sbralie 3350 unissb 4938 dftr2c 5263 axsepgfromrep 5292 nalset 5308 zfpow 5361 dtruALT2 5365 el 5434 dtruOLD 5438 zfun 7736 tz7.48lem 8456 coflton 8686 pssnn 9187 unxpdomlem1 9269 pssnnOLD 9284 zfinf 9657 aceq1 10135 aceq0 10136 aceq2 10137 dfac3 10139 dfac5lem2 10142 dfac5lem3 10143 dfac2a 10147 kmlem4 10171 zfac 10478 nd1 10605 axextnd 10609 axrepndlem1 10610 axrepndlem2 10611 axunndlem1 10613 axunnd 10614 axpowndlem2 10616 axpowndlem3 10617 axpowndlem4 10618 axregndlem1 10620 axregnd 10622 zfcndun 10633 zfcndpow 10634 zfcndinf 10636 zfcndac 10637 fpwwe2lem11 10659 axgroth3 10849 axgroth4 10850 nqereu 10947 mdetunilem9 22516 madugsum 22539 neiptopnei 23030 2ndc1stc 23349 nrmr0reg 23647 alexsubALTlem4 23948 xrsmopn 24722 itg2cn 25687 itgcn 25768 sqff1o 27108 dya2iocuni 33898 bnj849 34551 fineqvrep 34710 erdsze 34807 untsucf 35299 untangtr 35303 dfon2lem3 35376 dfon2lem6 35379 dfon2lem7 35380 dfon2 35383 axextdist 35390 distel 35394 neibastop2lem 35839 bj-elequ12 36150 bj-nfeel2 36326 bj-ru0 36416 prtlem5 38327 prtlem13 38335 prtlem16 38336 ax12el 38409 pw2f1ocnv 42449 aomclem8 42476 onsupmaxb 42658 grumnud 43714 lcosslsp 47497 |
Copyright terms: Public domain | W3C validator |