Theorem eleq2w 2853

Description: Weaker version of eleq2 2858 (but more general than elequ2 2164) not depending on ax-ext 2741 nor df-cleq 2761. (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 2164	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 641	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1948	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2845	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2845	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844

This theorem is referenced by:  clelsb2  2897  eluniab  4890  elintabg  4927  cantnflem1c  9658  tcrank  9858  isf32lem2  10340  sadcp1  16515  subgacs  19229  nsgacs  19230  sdrgacs  20884  lssacs  21068  elcls3  23211  conncompconn  23560  1stcfb  23573  dfac14lem  23745  r0cld  23866  uffix  24049  flftg  24124  tgpconncompeqg  24240  wilth  27203  tghilberti2  28875  prlngmolem2  29158  umgr2edgneu  29507  uspgredg2v  29517  usgredgleordALT  29527  nbusgrf1o  29664  vtxdushgrfvedglem  29782  constrmon  34081  ddemeas  34573  cvmcov  35690  cvmseu  35703  sat1el2xp  35806  hilbert1.2  36582  fneint  36784  mnuprdlem1  44911  mnuprdlem2  44912  mnuprdlem4  44914  elunif  45665  fnchoice  45678  lmbr3  46390