Theorem eleq2w 2818

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

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

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 2007  ax-8 2110  ax-9 2118

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

This theorem is referenced by:  clelsb2  2862  eluniab  4897  elintabg  4933  elintabOLD  4935  cantnflem1c  9701  tcrank  9898  isf32lem2  10368  sadcp1  16474  subgacs  19144  nsgacs  19145  sdrgacs  20761  lssacs  20924  elcls3  23021  conncompconn  23370  1stcfb  23383  dfac14lem  23555  r0cld  23676  uffix  23859  flftg  23934  tgpconncompeqg  24050  wilth  27033  tghilberti2  28617  umgr2edgneu  29193  uspgredg2v  29203  usgredgleordALT  29213  nbusgrf1o  29350  vtxdushgrfvedglem  29469  constrmon  33778  ddemeas  34267  cvmcov  35285  cvmseu  35298  sat1el2xp  35401  hilbert1.2  36173  fneint  36366  mnuprdlem1  44296  mnuprdlem2  44297  mnuprdlem4  44299  elunif  45040  fnchoice  45053  lmbr3  45776