Theorem eleq2w 2825

Description: Weaker version of eleq2 2830 (but more general than elequ2 2123) not depending on ax-ext 2708 nor df-cleq 2729. (Contributed by BJ, 29-Sep-2019.)

Assertion

Ref	Expression
eleq2w	⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Proof of Theorem eleq2w

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ2 2123	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1921	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2817	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2817	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108

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-8 2110  ax-9 2118

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816

This theorem is referenced by:  clelsb2  2869  eluniab  4921  elintabg  4957  elintabOLD  4959  cantnflem1c  9727  tcrank  9924  isf32lem2  10394  sadcp1  16492  subgacs  19179  nsgacs  19180  sdrgacs  20802  lssacs  20965  elcls3  23091  conncompconn  23440  1stcfb  23453  dfac14lem  23625  r0cld  23746  uffix  23929  flftg  24004  tgpconncompeqg  24120  wilth  27114  tghilberti2  28646  umgr2edgneu  29231  uspgredg2v  29241  usgredgleordALT  29251  nbusgrf1o  29388  vtxdushgrfvedglem  29507  constrmon  33785  ddemeas  34237  cvmcov  35268  cvmseu  35281  sat1el2xp  35384  hilbert1.2  36156  fneint  36349  mnuprdlem1  44291  mnuprdlem2  44292  mnuprdlem4  44294  elunif  45021  fnchoice  45034  lmbr3  45762