Theorem eleq2w 2823

Description: Weaker version of eleq2 2828 (but more general than elequ2 2121) not depending on ax-ext 2706 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 2121	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1919	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2815	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2815	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814

This theorem is referenced by:  clelsb2  2867  eluniab  4926  elintabg  4962  elintabOLD  4964  cantnflem1c  9725  tcrank  9922  isf32lem2  10392  sadcp1  16489  subgacs  19192  nsgacs  19193  sdrgacs  20819  lssacs  20983  elcls3  23107  conncompconn  23456  1stcfb  23469  dfac14lem  23641  r0cld  23762  uffix  23945  flftg  24020  tgpconncompeqg  24136  wilth  27129  tghilberti2  28661  umgr2edgneu  29246  uspgredg2v  29256  usgredgleordALT  29266  nbusgrf1o  29403  vtxdushgrfvedglem  29522  constrmon  33749  ddemeas  34217  cvmcov  35248  cvmseu  35261  sat1el2xp  35364  hilbert1.2  36137  fneint  36331  mnuprdlem1  44268  mnuprdlem2  44269  mnuprdlem4  44271  elunif  44954  fnchoice  44967  lmbr3  45703