Theorem eleq2s 2232

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 2204	. 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 1331   e. wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  elrabi  2832  opelopabsb  4177  epelg  4207  reg3exmidlemwe  4488  elxpi  4550  optocl  4610  fvmptss2  5489  fvmptssdm  5498  acexmidlemcase  5762  elmpocl  5961  mpoxopn0yelv  6129  tfr2a  6211  tfri1dALT  6241  2oconcl  6329  ecexr  6427  ectocld  6488  ecoptocl  6509  eroveu  6513  mapsnconst  6581  diffitest  6774  en2eqpr  6794  ctssdccl  6989  exmidonfinlem  7042  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  dmaddpqlem  7178  nqpi  7179  nq0nn  7243  0nsr  7550  suplocsrlempr  7608  cnm  7633  axaddcl  7665  axmulcl  7667  aprcl  8401  peano2uzs  9372  fzssnn  9841  fzossnn0  9945  rebtwn2zlemstep  10023  fldiv4p1lem1div2  10071  frecfzennn  10192  fser0const  10282  facnn  10466  bcpasc  10505  hashfzo0  10562  rexuz3  10755  rexanuz2  10756  r19.2uz  10758  cau4  10881  caubnd2  10882  climshft2  11068  climaddc1  11091  climmulc2  11093  climsubc1  11094  climsubc2  11095  climlec2  11103  climcau  11109  climcaucn  11113  iserabs  11237  binomlem  11245  isumshft  11252  cvgratgt0  11295  clim2divap  11302  ntrivcvgap  11310  infssuzex  11631  infssuzledc  11632  3prm  11798  phicl2  11879  phibndlem  11881  dfphi2  11885  crth  11889  phimullem  11890  znnen  11900  ennnfonelemkh  11914  bj-el2oss1o  12970  el2oss1o  13177  nninfalllem1  13192  nninfall  13193  isomninnlem  13214