Theorem eleq2s 2291

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 2263	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 121	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  elrabi  2917  opelopabsb  4295  epelg  4326  reg3exmidlemwe  4616  elxpi  4680  optocl  4740  elfvm  5594  fvmptss2  5639  fvmptssdm  5649  acexmidlemcase  5920  elmpocl  6122  mpoxopn0yelv  6306  tfr2a  6388  tfri1dALT  6418  2oconcl  6506  el2oss1o  6510  ecexr  6606  ectocld  6669  ecoptocl  6690  eroveu  6694  mapsnconst  6762  diffitest  6957  en2eqpr  6977  ctssdccl  7186  nninfwlpoimlemginf  7251  exmidonfinlem  7274  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  acnrcl  7286  dmaddpqlem  7463  nqpi  7464  nq0nn  7528  0nsr  7835  suplocsrlempr  7893  cnm  7918  axaddcl  7950  axmulcl  7952  aprcl  8692  aptap  8696  peano2uzs  9677  fzssnn  10162  fzossnn0  10270  infssuzex  10342  infssuzledc  10343  rebtwn2zlemstep  10361  fldiv4p1lem1div2  10414  frecfzennn  10537  fser0const  10646  facnn  10838  bcpasc  10877  hashfzo0  10934  rexuz3  11174  rexanuz2  11175  r19.2uz  11177  cau4  11300  caubnd2  11301  climshft2  11490  climaddc1  11513  climmulc2  11515  climsubc1  11516  climsubc2  11517  climlec2  11525  climcau  11531  climcaucn  11535  iserabs  11659  binomlem  11667  isumshft  11674  cvgratgt0  11717  clim2divap  11724  ntrivcvgap  11732  fprodntrivap  11768  fprodeq0  11801  3prm  12323  phicl2  12409  phibndlem  12411  dfphi2  12415  crth  12419  phimullem  12420  znnen  12642  ennnfonelemkh  12656  fvprif  13047  xpsfeq  13049  ismgmn0  13062  zrhval  14251  lgsdir2lem2  15378  lgsdir2lem3  15379  lgsquadlem2  15427  2lgslem1b  15438  bj-el2oss1o  15528  2o01f  15749  nninfalllem1  15763  nninfall  15764