Theorem eleq2s 2265

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 2237	. 2 |- ( A e. C <-> A e. B )
3		eleq2s.1	. 2 |- ( A e. B -> ph )
4	2, 3	sylbi 120	1 |- ( A e. C -> ph )

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  elrabi  2883  opelopabsb  4245  epelg  4275  reg3exmidlemwe  4563  elxpi  4627  optocl  4687  fvmptss2  5571  fvmptssdm  5580  acexmidlemcase  5848  elmpocl  6047  mpoxopn0yelv  6218  tfr2a  6300  tfri1dALT  6330  2oconcl  6418  el2oss1o  6422  ecexr  6518  ectocld  6579  ecoptocl  6600  eroveu  6604  mapsnconst  6672  diffitest  6865  en2eqpr  6885  ctssdccl  7088  nninfwlpoimlemginf  7152  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  dmaddpqlem  7339  nqpi  7340  nq0nn  7404  0nsr  7711  suplocsrlempr  7769  cnm  7794  axaddcl  7826  axmulcl  7828  aprcl  8565  peano2uzs  9543  fzssnn  10024  fzossnn0  10131  rebtwn2zlemstep  10209  fldiv4p1lem1div2  10261  frecfzennn  10382  fser0const  10472  facnn  10661  bcpasc  10700  hashfzo0  10758  rexuz3  10954  rexanuz2  10955  r19.2uz  10957  cau4  11080  caubnd2  11081  climshft2  11269  climaddc1  11292  climmulc2  11294  climsubc1  11295  climsubc2  11296  climlec2  11304  climcau  11310  climcaucn  11314  iserabs  11438  binomlem  11446  isumshft  11453  cvgratgt0  11496  clim2divap  11503  ntrivcvgap  11511  fprodntrivap  11547  fprodeq0  11580  infssuzex  11904  infssuzledc  11905  3prm  12082  phicl2  12168  phibndlem  12170  dfphi2  12174  crth  12178  phimullem  12179  znnen  12353  ennnfonelemkh  12367  ismgmn0  12612  lgsdir2lem2  13724  lgsdir2lem3  13725  bj-el2oss1o  13809  2o01f  14029  nninfalllem1  14041  nninfall  14042