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 2898 (but more general than elequ2 2120) not depending on ax-ext 2790 nor df-cleq 2811. (Contributed by BJ, 29-Sep-2019.) |
Ref | Expression |
---|---|
eleq2w | ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ2 2120 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | |
2 | 1 | anbi2d 628 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))) |
3 | 2 | exbidv 1913 | . 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))) |
4 | dfclel 2891 | . 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥)) | |
5 | dfclel 2891 | . 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)) | |
6 | 3, 4, 5 | 3bitr4g 315 | 1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ∃wex 1771 ∈ wcel 2105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-clel 2890 |
This theorem is referenced by: eluniab 4841 elintab 4878 cantnflem1c 9138 tcrank 9301 isf32lem2 9764 sadcp1 15792 subgacs 18251 nsgacs 18252 sdrgacs 19509 lssacs 19668 elcls3 21619 conncompconn 21968 1stcfb 21981 dfac14lem 22153 r0cld 22274 uffix 22457 flftg 22532 tgpconncompeqg 22647 wilth 25575 tghilberti2 26351 umgr2edgneu 26923 uspgredg2v 26933 usgredgleordALT 26943 nbusgrf1o 27080 vtxdushgrfvedglem 27198 ddemeas 31394 cvmcov 32407 cvmseu 32420 sat1el2xp 32523 hilbert1.2 33513 fneint 33593 elintabg 39812 mnuprdlem1 40485 mnuprdlem2 40486 mnuprdlem4 40488 elunif 41150 fnchoice 41163 lmbr3 41904 |
Copyright terms: Public domain | W3C validator |