Theorem eleq2s 2272

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 2244	. 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 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  elrabi  2890  opelopabsb  4258  epelg  4288  reg3exmidlemwe  4576  elxpi  4640  optocl  4700  fvmptss2  5588  fvmptssdm  5597  acexmidlemcase  5865  elmpocl  6064  mpoxopn0yelv  6235  tfr2a  6317  tfri1dALT  6347  2oconcl  6435  el2oss1o  6439  ecexr  6535  ectocld  6596  ecoptocl  6617  eroveu  6621  mapsnconst  6689  diffitest  6882  en2eqpr  6902  ctssdccl  7105  nninfwlpoimlemginf  7169  exmidonfinlem  7187  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  dmaddpqlem  7371  nqpi  7372  nq0nn  7436  0nsr  7743  suplocsrlempr  7801  cnm  7826  axaddcl  7858  axmulcl  7860  aprcl  8597  aptap  8601  peano2uzs  9578  fzssnn  10061  fzossnn0  10168  rebtwn2zlemstep  10246  fldiv4p1lem1div2  10298  frecfzennn  10419  fser0const  10509  facnn  10698  bcpasc  10737  hashfzo0  10794  rexuz3  10990  rexanuz2  10991  r19.2uz  10993  cau4  11116  caubnd2  11117  climshft2  11305  climaddc1  11328  climmulc2  11330  climsubc1  11331  climsubc2  11332  climlec2  11340  climcau  11346  climcaucn  11350  iserabs  11474  binomlem  11482  isumshft  11489  cvgratgt0  11532  clim2divap  11539  ntrivcvgap  11547  fprodntrivap  11583  fprodeq0  11616  infssuzex  11940  infssuzledc  11941  3prm  12118  phicl2  12204  phibndlem  12206  dfphi2  12210  crth  12214  phimullem  12215  znnen  12389  ennnfonelemkh  12403  ismgmn0  12707  lgsdir2lem2  14212  lgsdir2lem3  14213  bj-el2oss1o  14297  2o01f  14517  nninfalllem1  14528  nninfall  14529