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 2827 (but more general than elequ2 2121) not depending on ax-ext 2709 nor df-cleq 2730. (Contributed by BJ, 29-Sep-2019.) |
Ref | Expression |
---|---|
eleq2w | ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ2 2121 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
2 | 1 | anbi2d 629 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))) |
3 | 2 | exbidv 1924 | . 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))) |
4 | dfclel 2817 | . 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥)) | |
5 | dfclel 2817 | . 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∃wex 1782 ∈ wcel 2106 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-clel 2816 |
This theorem is referenced by: clelsb2 2867 eluniab 4854 elintab 4890 cantnflem1c 9445 tcrank 9642 isf32lem2 10110 sadcp1 16162 subgacs 18789 nsgacs 18790 sdrgacs 20069 lssacs 20229 elcls3 22234 conncompconn 22583 1stcfb 22596 dfac14lem 22768 r0cld 22889 uffix 23072 flftg 23147 tgpconncompeqg 23263 wilth 26220 tghilberti2 26999 umgr2edgneu 27581 uspgredg2v 27591 usgredgleordALT 27601 nbusgrf1o 27738 vtxdushgrfvedglem 27856 ddemeas 32204 cvmcov 33225 cvmseu 33238 sat1el2xp 33341 hilbert1.2 34457 fneint 34537 elintabg 41182 mnuprdlem1 41890 mnuprdlem2 41891 mnuprdlem4 41893 elunif 42559 fnchoice 42572 lmbr3 43288 |
Copyright terms: Public domain | W3C validator |