Theorem eleq2w 2822

Description: Weaker version of eleq2 2827 (but more general than elequ2 2122) not depending on ax-ext 2709 nor df-cleq 2730. (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 2122	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1925	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2817	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2817	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2816

This theorem is referenced by:  clelsb2  2867  eluniab  4879  elintabg  4917  elintabOLD  4919  cantnflem1c  9557  tcrank  9754  isf32lem2  10224  sadcp1  16271  subgacs  18898  nsgacs  18899  sdrgacs  20197  lssacs  20357  elcls3  22362  conncompconn  22711  1stcfb  22724  dfac14lem  22896  r0cld  23017  uffix  23200  flftg  23275  tgpconncompeqg  23391  wilth  26348  tghilberti2  27385  umgr2edgneu  27967  uspgredg2v  27977  usgredgleordALT  27987  nbusgrf1o  28124  vtxdushgrfvedglem  28242  ddemeas  32615  cvmcov  33637  cvmseu  33650  sat1el2xp  33753  hilbert1.2  34671  fneint  34751  mnuprdlem1  42353  mnuprdlem2  42354  mnuprdlem4  42356  elunif  43022  fnchoice  43035  lmbr3  43779