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  4885  elintabg  4921  elintabOLD  4923  cantnflem1c  9640  tcrank  9837  isf32lem2  10307  sadcp1  16425  subgacs  19093  nsgacs  19094  sdrgacs  20710  lssacs  20873  elcls3  22970  conncompconn  23319  1stcfb  23332  dfac14lem  23504  r0cld  23625  uffix  23808  flftg  23883  tgpconncompeqg  23999  wilth  26981  tghilberti2  28565  umgr2edgneu  29141  uspgredg2v  29151  usgredgleordALT  29161  nbusgrf1o  29298  vtxdushgrfvedglem  29417  constrmon  33734  ddemeas  34226  cvmcov  35250  cvmseu  35263  sat1el2xp  35366  hilbert1.2  36143  fneint  36336  mnuprdlem1  44261  mnuprdlem2  44262  mnuprdlem4  44264  elunif  45010  fnchoice  45023  lmbr3  45745