Theorem eleq2w 2844

Description: Weaker version of eleq2 2849 (but more general than elequ2 2159) not depending on ax-ext 2732 nor df-cleq 2752. (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 2159	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 642	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1953	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2836	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2836	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835

This theorem is used by:  clelsb2  2888  eluniab  4880  elintabg  4917  cantnflem1c  9688  tcrank  9901  isf32lem2  10432  sadcp1  16625  subgacs  19371  nsgacs  19372  sdrgacs  21058  lssacs  21242  elcls3  23401  conncompconn  23750  1stcfb  23763  dfac14lem  23936  r0cld  24057  uffix  24240  flftg  24315  tgpconncompeqg  24431  wilth  27398  tghilberti2  29106  prlngmolem2  29431  umgr2edgneu  29795  uspgredg2v  29805  usgredgleordALT  29815  nbusgrf1o  29952  vtxdushgrfvedglem  30070  constrmon  34376  ddemeas  34869  cvmcov  36028  cvmseu  36041  sat1el2xp  36144  hilbert1.2  36920  fneint  37136  mnuprdlem1  45256  mnuprdlem2  45257  mnuprdlem4  45259  elunif  46033  fnchoice  46046  lmbr3  46757