Theorem eleq2w 2817

Description: Weaker version of eleq2 2822 (but more general than elequ2 2121) not depending on ax-ext 2703 nor df-cleq 2724. (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 629	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1924	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2811	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2811	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2810

This theorem is referenced by:  clelsb2  2861  eluniab  4923  elintabg  4961  elintabOLD  4963  cantnflem1c  9684  tcrank  9881  isf32lem2  10351  sadcp1  16400  subgacs  19077  nsgacs  19078  sdrgacs  20560  lssacs  20722  elcls3  22807  conncompconn  23156  1stcfb  23169  dfac14lem  23341  r0cld  23462  uffix  23645  flftg  23720  tgpconncompeqg  23836  wilth  26799  tghilberti2  28144  umgr2edgneu  28726  uspgredg2v  28736  usgredgleordALT  28746  nbusgrf1o  28883  vtxdushgrfvedglem  29001  ddemeas  33520  cvmcov  34540  cvmseu  34553  sat1el2xp  34656  hilbert1.2  35419  fneint  35536  mnuprdlem1  43333  mnuprdlem2  43334  mnuprdlem4  43336  elunif  44002  fnchoice  44015  lmbr3  44762