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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  elrabi  2979  opelopabsb  4402  epelg  4435  reg3exmidlemwe  4726  elxpi  4790  optocl  4851  elfvm  5729  elfvfvex  5730  fvmbr  5731  fvmptss2  5780  fvmptssdm  5790  mptmex  5945  acexmidlemcase  6080  elmpocl  6284  ressuppss  6494  mpoxopn0yelv  6510  tfr2a  6592  tfri1dALT  6622  2oconcl  6712  el2oss1o  6716  ecexr  6812  ectocld  6875  ecoptocl  6896  eroveu  6900  mapsnconst  6976  diffitest  7191  en2eqpr  7214  ctssdccl  7451  nninfwlpoimlemginf  7516  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnrcl  7557  dmaddpqlem  7744  nqpi  7745  nq0nn  7809  0nsr  8116  suplocsrlempr  8174  cnm  8199  axaddcl  8231  axmulcl  8233  aprcl  8974  aptap  8978  peano2uzs  9984  fzssnn  10474  fzossnn0  10584  infssuzex  10666  infssuzledc  10667  rebtwn2zlemstep  10687  fldiv4p1lem1div2  10740  frecfzennn  10863  fser0const  10972  facnn  11165  bcpasc  11204  hashfzo0  11264  hashfibc  11283  ccatval2  11366  ccatass  11376  pfxclz  11451  wrdeqs1cat  11492  rexuz3  11756  rexanuz2  11757  r19.2uz  11759  cau4  11882  caubnd2  11883  climshft2  12072  climaddc1  12095  climmulc2  12097  climsubc1  12098  climsubc2  12099  climlec2  12107  climcau  12113  climcaucn  12117  iserabs  12242  binomlem  12250  isumshft  12257  cvgratgt0  12300  clim2divap  12307  ntrivcvgap  12315  fprodntrivap  12351  fprodeq0  12384  3prm  12906  phicl2  12992  phibndlem  12994  dfphi2  12998  crth  13002  phimullem  13003  ballotfilemfmpn  13234  znnen  13289  ennnfonelemkh  13303  fvprif  13664  xpsfeq  13666  ismgmn0  13678  mgpplusg  14222  mgpbas  14225  ringidval  14265  zrhval  14952  asclfval  15021  lgsdir2lem2  16148  lgsdir2lem3  16149  lgsquadlem2  16197  2lgslem1b  16208  1vgrex  16261  usgredg2v  16465  konigsberglem5  16733  bj-el2oss1o  16802  2o01f  17024  nninfalllem1  17051  nninfall  17052