Theorem eleq2s 2524

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 2498	. 2 |- ( A e. C <-> A e. B )
3		eleq2s.1	. 2 |- ( A e. B -> ph )
4	2, 3	sylbi 198	1 |- ( A e. C -> ph )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-cleq 2421  df-clel 2424

This theorem is referenced by:  elrabi  3168  epelg  4708  elxpi  4812  optocl  4873  eldmeldmressn  5107  predel  5359  fveqdmss  5976  oprabv  6297  elmpt2cl  6469  bropopvvv  6831  ressuppss  6889  mpt2xeldm  6912  mpt2xopn0yelv  6914  mpt2xopxnop0  6916  tfr2a  7068  rdgseg  7095  2oconcl  7160  ecexr  7323  ectocld  7385  ecoptocl  7408  brecop2  7412  eroveu  7413  mapsnconst  7472  mapfienlem1  7871  mapfienlem2  7872  mapfienlem3  7873  cantnflem2  8147  r1sucg  8192  r1suc  8193  acnrcl  8424  dfac5lem4  8508  fin23lem29  8722  fin23lem30  8723  axcclem  8838  alephval2  8948  0tsk  9131  0nsr  9454  peano2nn  10572  uzssz  11129  peano2uzs  11164  uzsupss  11207  fzssnn  11793  prednn0  11864  fzossnn0  11900  ltweuz  12125  fzennn  12131  ser1const  12219  expp1  12229  facnn  12411  facp1  12414  bcpasc  12456  hashfzo0  12550  ccatval2  12671  ccatass  12680  swrd00  12720  swrd0  12736  wrdeqs1cat  12777  splfv2a  12809  revccat  12817  rexuz3  13355  rexanuz2  13356  r19.2uz  13358  rexuzre  13359  cau4  13363  caubnd2  13364  climrlim2  13554  climshft2  13589  climaddc1  13641  climmulc2  13643  climsubc1  13644  climsubc2  13645  climlec2  13665  isercoll2  13675  climsup  13676  climcau  13677  caurcvg  13685  caurcvgOLD  13686  caurcvg2  13687  caucvg  13688  caucvgb  13689  iseraltlem1  13691  iseralt  13694  binomlem  13830  isumshft  13840  cvgrat  13882  clim2div  13888  ntrivcvg  13896  ntrivcvgtail  13899  fprodntriv  13939  fprodeq0  13972  fprodefsum  14092  3prm  14584  phicl2  14659  phibndlem  14661  dfphi2  14665  crt  14669  vdwap0  14869  prmlem1a  15021  xpscfv  15411  xpsfeq  15413  oppccofval  15564  homarcl2  15873  arwrcl  15882  pleval2i  16153  letsr  16416  gsumws1  16566  mulgpropd  16734  psgnunilem2  17079  psgnprfval  17105  gexid  17175  efgmnvl  17307  efgrcl  17308  efgsval  17324  efgs1  17328  efgs1b  17329  frgpuptinv  17364  frgpup3lem  17370  lt6abl  17472  eldprd  17579  isunit  17828  isirred  17870  abvrcl  17992  islss  18101  lbsss  18243  lbssp  18245  lbsind  18246  mpfrcl  18684  psr1basf  18737  coe1tm  18809  ply1frcl  18850  cssi  19189  thlle  19202  islbs4  19332  mavmulsolcl  19518  marepvcl  19536  1marepvmarrepid  19542  mdet0pr  19559  m2detleiblem1  19591  cramerimplem1  19650  cramerlem1  19654  chpscmat  19808  chpscmatgsumbin  19810  chpscmatgsummon  19811  ptpjpre1  20528  fin1aufil  20889  lmflf  20962  tsmsfbas  21084  xpsxmetlem  21336  xpsmet  21339  metustsym  21512  iscmet3lem3  22202  iscmet3lem1  22203  iscmet3lem2  22204  iscmet3  22205  rrxmvallem  22300  volsup  22451  opnmblALT  22503  itg1val  22583  tdeglem2  22952  ulmcaulem  23291  ulmcau  23292  ulmss  23294  pserdvlem2  23325  eff1olem  23439  logdmnrp  23528  dvlog2lem  23539  logtayl  23547  cxpcn3lem  23629  atancl  23749  atanval  23752  chp1  24036  ppiublem2  24073  lgsdir2lem2  24194  lgsdir2lem3  24195  lgsquadlem2  24225  rplogsumlem1  24264  rplogsumlem2  24265  pntlemj  24383  uhgrac  24974  usgraidx2v  25062  nbgraf1olem3  25113  nbgraf1olem5  25115  wwlkextproplem1  25411  wwlkextproplem2  25412  wwlkextproplem3  25413  clwwlknprop  25442  clwlkisclwwlklem2a4  25454  eleclclwwlknlem1  25487  eleclclwwlknlem2  25488  erclwwlkneqlen  25494  erclwwlknref  25495  erclwwlknsym  25496  erclwwlkntr  25497  clwlkf1clwwlk  25520  2wlkonot3v  25545  2spthonot3v  25546  frgrawopreglem4  25717  frgrawopreg  25719  gxnn0suc  25934  smgrpismgmOLD  26002  smgrpisass  26003  mndoissmgrpOLD  26009  mndoisexid  26010  drngoi  26077  rngoueqz  26100  vci  26109  axhcompl-zf  26593  mayete3i  27323  pj3lem1  27801  fzto1stfv1  28566  fzto1st  28568  fzto1stinvn  28569  psgnfzto1st  28570  submat1n  28583  xrge0mulc1cn  28699  fiunelros  28948  elmbfmvol2  29041  fibp1  29186  rrvsum  29239  ballotlemfmpn  29279  bnj529  29503  bnj923  29531  bnj570  29668  bnj594  29675  bnj1173  29763  bnj1256  29776  bnj1259  29777  bnj1296  29782  bnj1498  29822  subfacp1lem1  29854  kur14lem7  29887  mvrsval  30095  mvrsfpw  30096  mrsubcv  30100  mrsubccat  30108  msubff  30120  msrid  30135  msubvrs  30150  mppsval  30162  divcnvlin  30318  iprodefisumlem  30327  iprodefisum  30328  faclimlem1  30330  onsucsuccmpi  31052  bj-inftyexpidisj  31559  bj-ccinftydisj  31562  bj-elccinfty  31563  finixpnum  31837  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem8  31855  poimirlem9  31856  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem13  31860  poimirlem14  31861  poimirlem15  31862  poimirlem16  31863  poimirlem17  31864  poimirlem18  31865  poimirlem19  31866  poimirlem20  31867  poimirlem21  31868  poimirlem22  31869  poimirlem29  31876  poimirlem30  31877  broucube  31881  volsupnfl  31892  dvasin  31935  dvacos  31936  sdclem2  31978  fdc  31981  heiborlem4  32053  heiborlem6  32055  jm2.23  35764  wepwsolem  35813  trclfvdecomr  36233  binomcxplemdvbinom  36615  binomcxplemnotnn0  36618  ssfiunibd  37424  climinf  37567  climinfOLD  37568  stoweidlem15  37758  fourierdlem66  37919  etransclem37  38019  eldmressn  38438  afvres  38487  ndmaovrcl  38519  pfx00  38738  pfx0  38739  usgridx2v  39051  umgrres1lem  39114  upgrres1  39117  nbupgrres  39174  usgresvm1  39346  usgresvm1ALT  39350  2zrngamnd  39532  2zrngacmnd  39533  2zrngagrp  39534  2zrngALT  39539  2zrngnmlid  39540  2zrngnmlid2  39542  fldhmsubc  39677  fldhmsubcALTV  39696  lincvalsng  39802  snlindsntor  39857  lincresunit3lem2  39866  lincresunit3  39867  ldepsnlinc  39894  nn0sumshdiglemA  40023  nn0sumshdiglemB  40024