Theorem eleq2w 2828

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  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 1778  df-clel 2819

This theorem is referenced by:  clelsb2  2872  eluniab  4945  elintabg  4981  elintabOLD  4983  cantnflem1c  9756  tcrank  9953  isf32lem2  10423  sadcp1  16501  subgacs  19201  nsgacs  19202  sdrgacs  20824  lssacs  20988  elcls3  23112  conncompconn  23461  1stcfb  23474  dfac14lem  23646  r0cld  23767  uffix  23950  flftg  24025  tgpconncompeqg  24141  wilth  27132  tghilberti2  28664  umgr2edgneu  29249  uspgredg2v  29259  usgredgleordALT  29269  nbusgrf1o  29406  vtxdushgrfvedglem  29525  constrmon  33734  ddemeas  34200  cvmcov  35231  cvmseu  35244  sat1el2xp  35347  hilbert1.2  36119  fneint  36314  mnuprdlem1  44241  mnuprdlem2  44242  mnuprdlem4  44244  elunif  44916  fnchoice  44929  lmbr3  45668