Theorem eleq2w 2817

Description: Weaker version of eleq2 2822 (but more general than elequ2 2121) not depending on ax-ext 2703 nor df-cleq 2724. (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 2121	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 629	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1924	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2811	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2811	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 1782  df-clel 2810

This theorem is referenced by:  clelsb2  2861  eluniab  4923  elintabg  4961  elintabOLD  4963  cantnflem1c  9681  tcrank  9878  isf32lem2  10348  sadcp1  16395  subgacs  19040  nsgacs  19041  sdrgacs  20416  lssacs  20577  elcls3  22586  conncompconn  22935  1stcfb  22948  dfac14lem  23120  r0cld  23241  uffix  23424  flftg  23499  tgpconncompeqg  23615  wilth  26572  tghilberti2  27886  umgr2edgneu  28468  uspgredg2v  28478  usgredgleordALT  28488  nbusgrf1o  28625  vtxdushgrfvedglem  28743  ddemeas  33229  cvmcov  34249  cvmseu  34262  sat1el2xp  34365  hilbert1.2  35122  fneint  35228  mnuprdlem1  43021  mnuprdlem2  43022  mnuprdlem4  43024  elunif  43690  fnchoice  43703  lmbr3  44453