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  8976  aptap  8980  peano2uzs  9993  fzssnn  10484  fzossnn0  10594  infssuzex  10676  infssuzledc  10677  rebtwn2zlemstep  10697  fldiv4p1lem1div2  10753  frecfzennn  10876  fser0const  10985  facnn  11179  bcpasc  11218  hashfzo0  11278  hashfibc  11297  ccatval2  11380  ccatass  11390  pfxclz  11465  wrdeqs1cat  11506  rexuz3  11770  rexanuz2  11771  r19.2uz  11773  cau4  11897  caubnd2  11898  climshft2  12088  climaddc1  12111  climmulc2  12113  climsubc1  12114  climsubc2  12115  climlec2  12123  climcau  12129  climcaucn  12133  iserabs  12258  binomlem  12266  isumshft  12273  cvgratgt0  12316  clim2divap  12323  ntrivcvgap  12331  fprodntrivap  12367  fprodeq0  12400  3prm  12922  phicl2  13012  phibndlem  13014  dfphi2  13018  crth  13022  phimullem  13023  prmlem1a  13241  ballotfilemfmpn  13283  znnen  13338  ennnfonelemkh  13352  fvprif  13713  xpsfeq  13715  ismgmn0  13727  mgpplusg  14271  mgpbas  14274  ringidval  14314  zrhval  15001  asclfval  15070  ppiublem2  16193  lgsdir2lem2  16246  lgsdir2lem3  16247  lgsquadlem2  16295  2lgslem1b  16306  1vgrex  16359  usgredg2v  16563  konigsberglem5  16831  bj-el2oss1o  16900  2o01f  17122  nninfalllem1  17149  nninfall  17150