Theorem eleq2w 2821

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  clelsb2  2865  eluniab  4865  elintabg  4901  cantnflem1c  9603  tcrank  9803  isf32lem2  10271  sadcp1  16419  subgacs  19131  nsgacs  19132  sdrgacs  20773  lssacs  20957  elcls3  23062  conncompconn  23411  1stcfb  23424  dfac14lem  23596  r0cld  23717  uffix  23900  flftg  23975  tgpconncompeqg  24091  wilth  27052  tghilberti2  28724  umgr2edgneu  29301  uspgredg2v  29311  usgredgleordALT  29321  nbusgrf1o  29458  vtxdushgrfvedglem  29577  constrmon  33908  ddemeas  34400  cvmcov  35465  cvmseu  35478  sat1el2xp  35581  hilbert1.2  36357  fneint  36550  mnuprdlem1  44723  mnuprdlem2  44724  mnuprdlem4  44726  elunif  45471  fnchoice  45484  lmbr3  46199