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  7452  nninfwlpoimlemginf  7517  exmidonfinlem  7546  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acnrcl  7558  dmaddpqlem  7745  nqpi  7746  nq0nn  7810  0nsr  8117  suplocsrlempr  8175  cnm  8200  axaddcl  8232  axmulcl  8234  aprcl  8977  aptap  8981  peano2uzs  9994  fzssnn  10485  fzossnn0  10595  infssuzex  10677  infssuzledc  10678  rebtwn2zlemstep  10698  fldiv4p1lem1div2  10755  frecfzennn  10878  fser0const  10987  facnn  11181  bcpasc  11220  hashfzo0  11280  hashfibc  11299  ccatval2  11382  ccatass  11392  pfxclz  11467  wrdeqs1cat  11508  rexuz3  11772  rexanuz2  11773  r19.2uz  11775  cau4  11899  caubnd2  11900  climshft2  12091  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  climlec2  12126  climcau  12132  climcaucn  12136  iserabs  12261  binomlem  12269  isumshft  12276  cvgratgt0  12319  clim2divap  12326  ntrivcvgap  12334  fprodntrivap  12370  fprodeq0  12403  3prm  12925  phicl2  13015  phibndlem  13017  dfphi2  13021  crth  13025  phimullem  13026  prmlem1a  13244  ballotfilemfmpn  13286  znnen  13341  ennnfonelemkh  13355  ressmex  13472  fvprif  13717  xpsfeq  13719  ismgmn0  13731  cntrval  14145  cntzval  14147  cntzrcl  14153  mgpplusg  14306  mgpbas  14309  ringidval  14349  zrhval  15036  asclfval  15105  ppiublem2  16253  lgsdir2lem2  16314  lgsdir2lem3  16315  lgsquadlem2  16363  2lgslem1b  16374  1vgrex  16427  usgredg2v  16631  konigsberglem5  16899  bj-el2oss1o  16968  2o01f  17190  nninfalllem1  17217  nninfall  17218