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  9616  tcrank  9813  isf32lem2  10283  sadcp1  16401  subgacs  19075  nsgacs  19076  sdrgacs  20721  lssacs  20905  elcls3  23003  conncompconn  23352  1stcfb  23365  dfac14lem  23537  r0cld  23658  uffix  23841  flftg  23916  tgpconncompeqg  24032  wilth  27014  tghilberti2  28618  umgr2edgneu  29194  uspgredg2v  29204  usgredgleordALT  29214  nbusgrf1o  29351  vtxdushgrfvedglem  29470  constrmon  33727  ddemeas  34219  cvmcov  35243  cvmseu  35256  sat1el2xp  35359  hilbert1.2  36136  fneint  36329  mnuprdlem1  44254  mnuprdlem2  44255  mnuprdlem4  44257  elunif  45003  fnchoice  45016  lmbr3  45738