Theorem eleq2w 2813

Description: Weaker version of eleq2 2818 (but more general than elequ2 2124) not depending on ax-ext 2702 nor df-cleq 2722. (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 2805	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2805	. 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 2804

This theorem is referenced by:  clelsb2  2857  eluniab  4888  elintabg  4924  elintabOLD  4926  cantnflem1c  9647  tcrank  9844  isf32lem2  10314  sadcp1  16432  subgacs  19100  nsgacs  19101  sdrgacs  20717  lssacs  20880  elcls3  22977  conncompconn  23326  1stcfb  23339  dfac14lem  23511  r0cld  23632  uffix  23815  flftg  23890  tgpconncompeqg  24006  wilth  26988  tghilberti2  28572  umgr2edgneu  29148  uspgredg2v  29158  usgredgleordALT  29168  nbusgrf1o  29305  vtxdushgrfvedglem  29424  constrmon  33741  ddemeas  34233  cvmcov  35257  cvmseu  35270  sat1el2xp  35373  hilbert1.2  36150  fneint  36343  mnuprdlem1  44268  mnuprdlem2  44269  mnuprdlem4  44271  elunif  45017  fnchoice  45030  lmbr3  45752