Theorem eleq2w 2846

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569  ∃wex 1808   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-clel 2837

This theorem is used by:  clelsb2  2890  eluniab  4885  elintabg  4922  cantnflem1c  9654  tcrank  9854  isf32lem2  10344  sadcp1  16519  subgacs  19233  nsgacs  19234  sdrgacs  20915  lssacs  21099  elcls3  23251  conncompconn  23600  1stcfb  23613  dfac14lem  23785  r0cld  23906  uffix  24089  flftg  24164  tgpconncompeqg  24280  wilth  27246  tghilberti2  28922  prlngmolem2  29214  umgr2edgneu  29575  uspgredg2v  29585  usgredgleordALT  29595  nbusgrf1o  29732  vtxdushgrfvedglem  29850  constrmon  34143  ddemeas  34635  cvmcov  35763  cvmseu  35776  sat1el2xp  35879  hilbert1.2  36655  fneint  36887  mnuprdlem1  45010  mnuprdlem2  45011  mnuprdlem4  45013  elunif  45764  fnchoice  45777  lmbr3  46489