![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eleq2w | Structured version Visualization version GIF version |
Description: Weaker version of eleq2 2823 (but more general than elequ2 2122) not depending on ax-ext 2704 nor df-cleq 2725. (Contributed by BJ, 29-Sep-2019.) |
Ref | Expression |
---|---|
eleq2w | ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ2 2122 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
2 | 1 | anbi2d 630 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))) |
3 | 2 | exbidv 1925 | . 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))) |
4 | dfclel 2812 | . 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥)) | |
5 | dfclel 2812 | . 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-clel 2811 |
This theorem is referenced by: clelsb2 2862 eluniab 4884 elintabg 4922 elintabOLD 4924 cantnflem1c 9631 tcrank 9828 isf32lem2 10298 sadcp1 16343 subgacs 18971 nsgacs 18972 sdrgacs 20311 lssacs 20472 elcls3 22457 conncompconn 22806 1stcfb 22819 dfac14lem 22991 r0cld 23112 uffix 23295 flftg 23370 tgpconncompeqg 23486 wilth 26443 tghilberti2 27629 umgr2edgneu 28211 uspgredg2v 28221 usgredgleordALT 28231 nbusgrf1o 28368 vtxdushgrfvedglem 28486 ddemeas 32899 cvmcov 33921 cvmseu 33934 sat1el2xp 34037 hilbert1.2 34793 fneint 34873 mnuprdlem1 42644 mnuprdlem2 42645 mnuprdlem4 42647 elunif 43313 fnchoice 43326 lmbr3 44078 |
Copyright terms: Public domain | W3C validator |