Theorem eleq2w 2825

Description: Weaker version of eleq2 2830 (but more general than elequ2 2136) not depending on ax-ext 2713 nor df-cleq 2733. (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 2136	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 637	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1929	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2817	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2817	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  ∃wex 1787   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-clel 2816

This theorem is referenced by:  clelsb2  2869  eluniab  4855  elintabg  4891  cantnflem1c  9603  tcrank  9803  isf32lem2  10271  sadcp1  16419  subgacs  19131  nsgacs  19132  sdrgacs  20777  lssacs  20961  elcls3  23070  conncompconn  23419  1stcfb  23432  dfac14lem  23604  r0cld  23725  uffix  23908  flftg  23983  tgpconncompeqg  24099  wilth  27056  tghilberti2  28728  umgr2edgneu  29305  uspgredg2v  29315  usgredgleordALT  29325  nbusgrf1o  29462  vtxdushgrfvedglem  29580  constrmon  33940  ddemeas  34432  cvmcov  35506  cvmseu  35519  sat1el2xp  35622  hilbert1.2  36398  fneint  36591  mnuprdlem1  44731  mnuprdlem2  44732  mnuprdlem4  44734  elunif  45479  fnchoice  45492  lmbr3  46204