Theorem eleq2w 2816

Description: Weaker version of eleq2 2821 (but more general than elequ2 2129) not depending on ax-ext 2710 nor df-cleq 2730. (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 2129	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1928	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2812	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2812	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542  ∃wex 1786   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-clel 2811

This theorem is referenced by:  eluniab  4811  elintab  4847  cantnflem1c  9223  tcrank  9386  isf32lem2  9854  sadcp1  15898  subgacs  18431  nsgacs  18432  sdrgacs  19699  lssacs  19858  elcls3  21834  conncompconn  22183  1stcfb  22196  dfac14lem  22368  r0cld  22489  uffix  22672  flftg  22747  tgpconncompeqg  22863  wilth  25808  tghilberti2  26584  umgr2edgneu  27156  uspgredg2v  27166  usgredgleordALT  27176  nbusgrf1o  27313  vtxdushgrfvedglem  27431  ddemeas  31774  cvmcov  32796  cvmseu  32809  sat1el2xp  32912  hilbert1.2  34095  fneint  34175  elintabg  40727  mnuprdlem1  41432  mnuprdlem2  41433  mnuprdlem4  41435  elunif  42097  fnchoice  42110  lmbr3  42830