Theorem eleq2w 2844

Description: Weaker version of eleq2 2849 (but more general than elequ2 2160) 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 2160	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 642	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1954	. 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 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 2835

This theorem is used by:  clelsb2  2888  eluniab  4880  elintabg  4917  cantnflem1c  9666  tcrank  9874  isf32lem2  10403  sadcp1  16592  subgacs  19332  nsgacs  19333  sdrgacs  21019  lssacs  21203  elcls3  23362  conncompconn  23711  1stcfb  23724  dfac14lem  23897  r0cld  24018  uffix  24201  flftg  24276  tgpconncompeqg  24392  wilth  27361  tghilberti2  29039  prlngmolem2  29364  umgr2edgneu  29728  uspgredg2v  29738  usgredgleordALT  29748  nbusgrf1o  29885  vtxdushgrfvedglem  30003  constrmon  34309  ddemeas  34802  cvmcov  35949  cvmseu  35962  sat1el2xp  36065  hilbert1.2  36842  fneint  37058  mnuprdlem1  45200  mnuprdlem2  45201  mnuprdlem4  45203  elunif  45954  fnchoice  45967  lmbr3  46679