Theorem eleq2w 2846

Description: Weaker version of eleq2 2851 (but more general than elequ2 2160) 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 2160	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 642	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1954	. 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 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2837

This theorem is used by:  clelsb2  2890  eluniab  4884  elintabg  4921  cantnflem1c  9669  tcrank  9869  isf32lem2  10359  sadcp1  16549  subgacs  19285  nsgacs  19286  sdrgacs  20968  lssacs  21152  elcls3  23309  conncompconn  23658  1stcfb  23671  dfac14lem  23844  r0cld  23965  uffix  24148  flftg  24223  tgpconncompeqg  24339  wilth  27305  tghilberti2  28983  prlngmolem2  29296  umgr2edgneu  29660  uspgredg2v  29670  usgredgleordALT  29680  nbusgrf1o  29817  vtxdushgrfvedglem  29935  constrmon  34241  ddemeas  34734  cvmcov  35829  cvmseu  35842  sat1el2xp  35945  hilbert1.2  36722  fneint  36954  mnuprdlem1  45083  mnuprdlem2  45084  mnuprdlem4  45086  elunif  45837  fnchoice  45850  lmbr3  46562