Theorem eleq2s 2333

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  elrabi  2979  opelopabsb  4400  epelg  4433  reg3exmidlemwe  4724  elxpi  4788  optocl  4849  elfvm  5726  elfvfvex  5727  fvmbr  5728  fvmptss2  5777  fvmptssdm  5787  mptmex  5939  acexmidlemcase  6074  elmpocl  6278  ressuppss  6488  mpoxopn0yelv  6504  tfr2a  6586  tfri1dALT  6616  2oconcl  6706  el2oss1o  6710  ecexr  6806  ectocld  6869  ecoptocl  6890  eroveu  6894  mapsnconst  6970  diffitest  7185  en2eqpr  7208  ctssdccl  7445  nninfwlpoimlemginf  7510  exmidonfinlem  7539  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  acnrcl  7551  dmaddpqlem  7738  nqpi  7739  nq0nn  7803  0nsr  8110  suplocsrlempr  8168  cnm  8193  axaddcl  8225  axmulcl  8227  aprcl  8968  aptap  8972  peano2uzs  9967  fzssnn  10457  fzossnn0  10567  infssuzex  10649  infssuzledc  10650  rebtwn2zlemstep  10670  fldiv4p1lem1div2  10723  frecfzennn  10846  fser0const  10955  facnn  11148  bcpasc  11187  hashfzo0  11247  hashfibc  11266  ccatval2  11349  ccatass  11359  pfxclz  11434  wrdeqs1cat  11475  rexuz3  11739  rexanuz2  11740  r19.2uz  11742  cau4  11865  caubnd2  11866  climshft2  12055  climaddc1  12078  climmulc2  12080  climsubc1  12081  climsubc2  12082  climlec2  12090  climcau  12096  climcaucn  12100  iserabs  12225  binomlem  12233  isumshft  12240  cvgratgt0  12283  clim2divap  12290  ntrivcvgap  12298  fprodntrivap  12334  fprodeq0  12367  3prm  12889  phicl2  12975  phibndlem  12977  dfphi2  12981  crth  12985  phimullem  12986  ballotfilemfmpn  13217  znnen  13272  ennnfonelemkh  13286  fvprif  13647  xpsfeq  13649  ismgmn0  13661  mgpplusg  14205  mgpbas  14208  ringidval  14248  zrhval  14935  asclfval  15004  lgsdir2lem2  16131  lgsdir2lem3  16132  lgsquadlem2  16180  2lgslem1b  16191  1vgrex  16244  usgredg2v  16448  konigsberglem5  16716  bj-el2oss1o  16785  2o01f  17007  nninfalllem1  17025  nninfall  17026