Theorem eleq2w 2821

Description: Weaker version of eleq2 2826 (but more general than elequ2 2129) not depending on ax-ext 2709 nor df-cleq 2729. (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 2813	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2813	. 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 2812

This theorem is referenced by:  clelsb2  2865  eluniab  4879  elintabg  4915  cantnflem1c  9610  tcrank  9810  isf32lem2  10278  sadcp1  16396  subgacs  19107  nsgacs  19108  sdrgacs  20751  lssacs  20935  elcls3  23044  conncompconn  23393  1stcfb  23406  dfac14lem  23578  r0cld  23699  uffix  23882  flftg  23957  tgpconncompeqg  24073  wilth  27054  tghilberti2  28728  umgr2edgneu  29305  uspgredg2v  29315  usgredgleordALT  29325  nbusgrf1o  29462  vtxdushgrfvedglem  29581  constrmon  33928  ddemeas  34420  cvmcov  35485  cvmseu  35498  sat1el2xp  35601  hilbert1.2  36377  fneint  36570  mnuprdlem1  44657  mnuprdlem2  44658  mnuprdlem4  44660  elunif  45405  fnchoice  45418  lmbr3  46134