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	|- ( A e. B -> ph )
eleq2s.2	|- C = B

Assertion

Ref	Expression
eleq2s	|- ( A e. C -> ph )

Proof of Theorem eleq2s

Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3 |- C = B
2	1	eleq2i 2305	. 2 |- ( A e. C <-> A e. B )
3		eleq2s.1	. 2 |- ( A e. B -> ph )
4	2, 3	sylbi 121	1 |- ( A e. C -> ph )

Syntax hints:   -> wi 4   = wceq 1402   e. 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  4397  epelg  4430  reg3exmidlemwe  4721  elxpi  4785  optocl  4846  elfvm  5723  elfvfvex  5724  fvmbr  5725  fvmptss2  5774  fvmptssdm  5784  acexmidlemcase  6070  elmpocl  6274  ressuppss  6484  mpoxopn0yelv  6500  tfr2a  6582  tfri1dALT  6612  2oconcl  6702  el2oss1o  6706  ecexr  6802  ectocld  6865  ecoptocl  6886  eroveu  6890  mapsnconst  6966  diffitest  7181  en2eqpr  7204  ctssdccl  7441  nninfwlpoimlemginf  7506  exmidonfinlem  7535  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  acnrcl  7547  dmaddpqlem  7734  nqpi  7735  nq0nn  7799  0nsr  8106  suplocsrlempr  8164  cnm  8189  axaddcl  8221  axmulcl  8223  aprcl  8964  aptap  8968  peano2uzs  9963  fzssnn  10452  fzossnn0  10562  infssuzex  10644  infssuzledc  10645  rebtwn2zlemstep  10665  fldiv4p1lem1div2  10718  frecfzennn  10841  fser0const  10950  facnn  11143  bcpasc  11182  hashfzo0  11242  hashfibc  11261  ccatval2  11344  ccatass  11354  pfxclz  11429  wrdeqs1cat  11470  rexuz3  11734  rexanuz2  11735  r19.2uz  11737  cau4  11860  caubnd2  11861  climshft2  12050  climaddc1  12073  climmulc2  12075  climsubc1  12076  climsubc2  12077  climlec2  12085  climcau  12091  climcaucn  12095  iserabs  12220  binomlem  12228  isumshft  12235  cvgratgt0  12278  clim2divap  12285  ntrivcvgap  12293  fprodntrivap  12329  fprodeq0  12362  3prm  12884  phicl2  12970  phibndlem  12972  dfphi2  12976  crth  12980  phimullem  12981  ballotfilemfmpn  13212  znnen  13267  ennnfonelemkh  13281  fvprif  13641  xpsfeq  13643  ismgmn0  13655  zrhval  14924  lgsdir2lem2  16062  lgsdir2lem3  16063  lgsquadlem2  16111  2lgslem1b  16122  1vgrex  16175  usgredg2v  16379  konigsberglem5  16647  bj-el2oss1o  16716  2o01f  16938  nninfalllem1  16956  nninfall  16957