Theorem eleq2w 2853

Description: Weaker version of eleq2 2858 (but more general than elequ2 2164) not depending on ax-ext 2741 nor df-cleq 2761. (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 2164	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 641	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1948	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2845	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2845	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844

This theorem is referenced by:  clelsb2  2897  eluniab  4888  elintabg  4925  cantnflem1c  9656  tcrank  9856  isf32lem2  10338  sadcp1  16513  subgacs  19227  nsgacs  19228  sdrgacs  20882  lssacs  21066  elcls3  23209  conncompconn  23558  1stcfb  23571  dfac14lem  23743  r0cld  23864  uffix  24047  flftg  24122  tgpconncompeqg  24238  wilth  27201  tghilberti2  28873  prlngmolem2  29156  umgr2edgneu  29505  uspgredg2v  29515  usgredgleordALT  29525  nbusgrf1o  29662  vtxdushgrfvedglem  29780  constrmon  34079  ddemeas  34571  cvmcov  35688  cvmseu  35701  sat1el2xp  35804  hilbert1.2  36580  fneint  36782  mnuprdlem1  44909  mnuprdlem2  44910  mnuprdlem4  44912  elunif  45663  fnchoice  45676  lmbr3  46388