Theorem eleq2w 2812

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803

This theorem is referenced by:  clelsb2  2856  eluniab  4881  elintabg  4917  elintabOLD  4919  cantnflem1c  9618  tcrank  9815  isf32lem2  10285  sadcp1  16402  subgacs  19076  nsgacs  19077  sdrgacs  20722  lssacs  20906  elcls3  23004  conncompconn  23353  1stcfb  23366  dfac14lem  23538  r0cld  23659  uffix  23842  flftg  23917  tgpconncompeqg  24033  wilth  27015  tghilberti2  28619  umgr2edgneu  29195  uspgredg2v  29205  usgredgleordALT  29215  nbusgrf1o  29352  vtxdushgrfvedglem  29471  constrmon  33728  ddemeas  34220  cvmcov  35244  cvmseu  35257  sat1el2xp  35360  hilbert1.2  36137  fneint  36330  mnuprdlem1  44255  mnuprdlem2  44256  mnuprdlem4  44258  elunif  45004  fnchoice  45017  lmbr3  45739