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  7272  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  acnrcl  7284  dmaddpqlem  7461  nqpi  7462  nq0nn  7526  0nsr  7833  suplocsrlempr  7891  cnm  7916  axaddcl  7948  axmulcl  7950  aprcl  8690  aptap  8694  peano2uzs  9675  fzssnn  10160  fzossnn0  10268  infssuzex  10340  infssuzledc  10341  rebtwn2zlemstep  10359  fldiv4p1lem1div2  10412  frecfzennn  10535  fser0const  10644  facnn  10836  bcpasc  10875  hashfzo0  10932  rexuz3  11172  rexanuz2  11173  r19.2uz  11175  cau4  11298  caubnd2  11299  climshft2  11488  climaddc1  11511  climmulc2  11513  climsubc1  11514  climsubc2  11515  climlec2  11523  climcau  11529  climcaucn  11533  iserabs  11657  binomlem  11665  isumshft  11672  cvgratgt0  11715  clim2divap  11722  ntrivcvgap  11730  fprodntrivap  11766  fprodeq0  11799  3prm  12321  phicl2  12407  phibndlem  12409  dfphi2  12413  crth  12417  phimullem  12418  znnen  12640  ennnfonelemkh  12654  fvprif  13045  xpsfeq  13047  ismgmn0  13060  zrhval  14249  lgsdir2lem2  15354  lgsdir2lem3  15355  lgsquadlem2  15403  2lgslem1b  15414  bj-el2oss1o  15504  2o01f  15725  nninfalllem1  15739  nninfall  15740