Theorem eleq2w 2819

Description: Weaker version of eleq2 2824 (but more general than elequ2 2129) not depending on ax-ext 2707 nor df-cleq 2727. (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 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1923	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2811	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2811	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2810

This theorem is referenced by:  clelsb2  2863  eluniab  4854  elintabg  4890  cantnflem1c  9597  tcrank  9797  isf32lem2  10265  sadcp1  16413  subgacs  19125  nsgacs  19126  sdrgacs  20767  lssacs  20951  elcls3  23036  conncompconn  23385  1stcfb  23398  dfac14lem  23570  r0cld  23691  uffix  23874  flftg  23949  tgpconncompeqg  24065  wilth  27022  tghilberti2  28694  umgr2edgneu  29271  uspgredg2v  29281  usgredgleordALT  29291  nbusgrf1o  29428  vtxdushgrfvedglem  29546  constrmon  33876  ddemeas  34368  cvmcov  35433  cvmseu  35446  sat1el2xp  35549  hilbert1.2  36325  fneint  36518  mnuprdlem1  44687  mnuprdlem2  44688  mnuprdlem4  44690  elunif  45435  fnchoice  45448  lmbr3  46163