Theorem eleq2w 2848

Description: Weaker version of eleq2 2853 (but more general than elequ2 2162) not depending on ax-ext 2735 nor df-cleq 2755. (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 2162	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 642	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1956	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2840	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2840	. 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 2147

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157

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

This theorem is used by:  clelsb2  2892  eluniab  4884  elintabg  4921  cantnflem1c  9712  tcrank  9925  isf32lem2  10456  sadcp1  16651  subgacs  19397  nsgacs  19398  sdrgacs  21085  lssacs  21269  elcls3  23428  conncompconn  23777  1stcfb  23790  dfac14lem  23963  r0cld  24084  uffix  24267  flftg  24342  tgpconncompeqg  24458  wilth  27425  tghilberti2  29133  prlngmolem2  29458  umgr2edgneu  29822  uspgredg2v  29832  usgredgleordALT  29842  nbusgrf1o  29979  vtxdushgrfvedglem  30097  constrmon  34443  ddemeas  34936  cvmcov  36194  cvmseu  36207  sat1el2xp  36310  hilbert1.2  37097  fneint  37313  mnuprdlem1  45446  mnuprdlem2  45447  mnuprdlem4  45449  elunif  46236  fnchoice  46249  lmbr3  46960