Theorem eleq2s 2301

Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
eleq2s.1	⊢ (𝐴 ∈ 𝐵 → 𝜑)
eleq2s.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleq2s	⊢ (𝐴 ∈ 𝐶 → 𝜑)

Proof of Theorem eleq2s

Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3 ⊢ 𝐶 = 𝐵
2	1	eleq2i 2273	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 121	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  elrabi  2927  opelopabsb  4310  epelg  4341  reg3exmidlemwe  4631  elxpi  4695  optocl  4755  elfvm  5616  fvmptss2  5661  fvmptssdm  5671  acexmidlemcase  5946  elmpocl  6148  mpoxopn0yelv  6332  tfr2a  6414  tfri1dALT  6444  2oconcl  6532  el2oss1o  6536  ecexr  6632  ectocld  6695  ecoptocl  6716  eroveu  6720  mapsnconst  6788  diffitest  6991  en2eqpr  7011  ctssdccl  7220  nninfwlpoimlemginf  7285  exmidonfinlem  7308  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  acnrcl  7320  dmaddpqlem  7497  nqpi  7498  nq0nn  7562  0nsr  7869  suplocsrlempr  7927  cnm  7952  axaddcl  7984  axmulcl  7986  aprcl  8726  aptap  8730  peano2uzs  9712  fzssnn  10197  fzossnn0  10306  infssuzex  10383  infssuzledc  10384  rebtwn2zlemstep  10402  fldiv4p1lem1div2  10455  frecfzennn  10578  fser0const  10687  facnn  10879  bcpasc  10918  hashfzo0  10975  ccatval2  11062  ccatass  11072  rexuz3  11345  rexanuz2  11346  r19.2uz  11348  cau4  11471  caubnd2  11472  climshft2  11661  climaddc1  11684  climmulc2  11686  climsubc1  11687  climsubc2  11688  climlec2  11696  climcau  11702  climcaucn  11706  iserabs  11830  binomlem  11838  isumshft  11845  cvgratgt0  11888  clim2divap  11895  ntrivcvgap  11903  fprodntrivap  11939  fprodeq0  11972  3prm  12494  phicl2  12580  phibndlem  12582  dfphi2  12586  crth  12590  phimullem  12591  znnen  12813  ennnfonelemkh  12827  fvprif  13219  xpsfeq  13221  ismgmn0  13234  zrhval  14423  lgsdir2lem2  15550  lgsdir2lem3  15551  lgsquadlem2  15599  2lgslem1b  15610  1vgrex  15663  bj-el2oss1o  15784  2o01f  16005  nninfalllem1  16019  nninfall  16020