Theorem eleq2s 2324

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 2296	. 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 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  elrabi  2956  opelopabsb  4347  epelg  4380  reg3exmidlemwe  4670  elxpi  4734  optocl  4794  elfvm  5659  elfvex  5660  fvmbr  5661  fvmptss2  5708  fvmptssdm  5718  acexmidlemcase  5995  elmpocl  6199  mpoxopn0yelv  6383  tfr2a  6465  tfri1dALT  6495  2oconcl  6583  el2oss1o  6587  ecexr  6683  ectocld  6746  ecoptocl  6767  eroveu  6771  mapsnconst  6839  diffitest  7045  en2eqpr  7065  ctssdccl  7274  nninfwlpoimlemginf  7339  exmidonfinlem  7367  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  acnrcl  7379  dmaddpqlem  7560  nqpi  7561  nq0nn  7625  0nsr  7932  suplocsrlempr  7990  cnm  8015  axaddcl  8047  axmulcl  8049  aprcl  8789  aptap  8793  peano2uzs  9775  fzssnn  10260  fzossnn0  10369  infssuzex  10448  infssuzledc  10449  rebtwn2zlemstep  10467  fldiv4p1lem1div2  10520  frecfzennn  10643  fser0const  10752  facnn  10944  bcpasc  10983  hashfzo0  11040  ccatval2  11128  ccatass  11138  pfxclz  11206  wrdeqs1cat  11247  rexuz3  11496  rexanuz2  11497  r19.2uz  11499  cau4  11622  caubnd2  11623  climshft2  11812  climaddc1  11835  climmulc2  11837  climsubc1  11838  climsubc2  11839  climlec2  11847  climcau  11853  climcaucn  11857  iserabs  11981  binomlem  11989  isumshft  11996  cvgratgt0  12039  clim2divap  12046  ntrivcvgap  12054  fprodntrivap  12090  fprodeq0  12123  3prm  12645  phicl2  12731  phibndlem  12733  dfphi2  12737  crth  12741  phimullem  12742  znnen  12964  ennnfonelemkh  12978  fvprif  13371  xpsfeq  13373  ismgmn0  13386  zrhval  14575  lgsdir2lem2  15702  lgsdir2lem3  15703  lgsquadlem2  15751  2lgslem1b  15762  1vgrex  15815  usgredg2v  16016  bj-el2oss1o  16096  2o01f  16317  nninfalllem1  16333  nninfall  16334