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  4404  epelg  4437  reg3exmidlemwe  4728  elxpi  4792  optocl  4853  elfvm  5732  elfvfvex  5733  fvmbr  5734  fvmptss2  5783  fvmptssdm  5793  mptmex  5948  acexmidlemcase  6083  elmpocl  6287  ressuppss  6498  mpoxopn0yelv  6515  tfr2a  6597  tfri1dALT  6627  2oconcl  6717  el2oss1o  6721  ecexr  6817  ectocld  6880  ecoptocl  6901  eroveu  6905  mapsnconst  6982  diffitest  7197  en2eqpr  7220  ctssdccl  7457  nninfwlpoimlemginf  7522  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acnrcl  7563  dmaddpqlem  7750  nqpi  7751  nq0nn  7815  0nsr  8122  suplocsrlempr  8180  cnm  8205  axaddcl  8237  axmulcl  8239  aprcl  8982  aptap  8986  peano2uzs  9999  fzssnn  10490  fzossnn0  10600  infssuzex  10682  infssuzledc  10683  rebtwn2zlemstep  10703  fldiv4p1lem1div2  10760  frecfzennn  10883  fser0const  10992  facnn  11186  bcpasc  11225  hashfzo0  11285  hashfibc  11304  ccatval2  11387  ccatass  11397  pfxclz  11472  wrdeqs1cat  11513  rexuz3  11777  rexanuz2  11778  r19.2uz  11780  cau4  11904  caubnd2  11905  climshft2  12096  climaddc1  12119  climmulc2  12121  climsubc1  12122  climsubc2  12123  climlec2  12131  climcau  12137  climcaucn  12141  iserabs  12266  binomlem  12274  isumshft  12281  cvgratgt0  12324  clim2divap  12331  ntrivcvgap  12339  fprodntrivap  12375  fprodeq0  12408  3prm  12930  phicl2  13020  phibndlem  13022  dfphi2  13026  crth  13030  phimullem  13031  prmlem1a  13249  ballotfilemfmpn  13291  znnen  13346  ennnfonelemkh  13360  ressmex  13477  fvprif  13722  xpsfeq  13724  ismgmn0  13736  cntrval  14150  cntzval  14152  cntzrcl  14158  mgpplusg  14328  mgpbas  14331  ringidval  14371  zrhval  15060  asclfval  15129  gsumbagdiagfi  15185  ppiublem2  16309  lgsdir2lem2  16370  lgsdir2lem3  16371  lgsquadlem2  16419  2lgslem1b  16430  1vgrex  16483  usgredg2v  16687  konigsberglem5  16955  bj-el2oss1o  17024  2o01f  17246  idjudju  17269  nninfalllem1  17274  nninfall  17275