Theorem eleq2w 2873

Description: Weaker version of eleq2 2878 (but more general than elequ2 2126) not depending on ax-ext 2770 nor df-cleq 2791. (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 2126	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1922	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2871	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2871	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2870

This theorem is referenced by:  eluniab  4815  elintab  4849  cantnflem1c  9134  tcrank  9297  isf32lem2  9765  sadcp1  15794  subgacs  18305  nsgacs  18306  sdrgacs  19573  lssacs  19732  elcls3  21688  conncompconn  22037  1stcfb  22050  dfac14lem  22222  r0cld  22343  uffix  22526  flftg  22601  tgpconncompeqg  22717  wilth  25656  tghilberti2  26432  umgr2edgneu  27004  uspgredg2v  27014  usgredgleordALT  27024  nbusgrf1o  27161  vtxdushgrfvedglem  27279  ddemeas  31605  cvmcov  32623  cvmseu  32636  sat1el2xp  32739  hilbert1.2  33729  fneint  33809  elintabg  40274  mnuprdlem1  40980  mnuprdlem2  40981  mnuprdlem4  40983  elunif  41645  fnchoice  41658  lmbr3  42389  issal  42956