Theorem eleq2w 2822

Description: Weaker version of eleq2 2827 (but more general than elequ2 2123) not depending on ax-ext 2709 nor df-cleq 2730. (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 628	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1925	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2818	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2818	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817

This theorem is referenced by:  eluniab  4851  elintab  4887  cantnflem1c  9375  tcrank  9573  isf32lem2  10041  sadcp1  16090  subgacs  18704  nsgacs  18705  sdrgacs  19984  lssacs  20144  elcls3  22142  conncompconn  22491  1stcfb  22504  dfac14lem  22676  r0cld  22797  uffix  22980  flftg  23055  tgpconncompeqg  23171  wilth  26125  tghilberti2  26903  umgr2edgneu  27484  uspgredg2v  27494  usgredgleordALT  27504  nbusgrf1o  27641  vtxdushgrfvedglem  27759  ddemeas  32104  cvmcov  33125  cvmseu  33138  sat1el2xp  33241  hilbert1.2  34384  fneint  34464  elintabg  41071  mnuprdlem1  41779  mnuprdlem2  41780  mnuprdlem4  41782  elunif  42448  fnchoice  42461  lmbr3  43178