Theorem eleq2s 2525

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429

This theorem is referenced by:  elrabi  3103  epelg  4620  elxpi  4843  optocl  4900  elmpt2cl  6293  bropopvvv  6642  ressuppss  6697  mpt2xopn0yelv  6719  mpt2xopxnop0  6721  tfr2a  6840  rdgseg  6864  2oconcl  6931  ecexr  7094  ectocld  7155  ecoptocl  7178  brecop2  7182  eroveu  7183  mapsnconst  7246  mapfienlem1  7642  mapfienlem2  7643  mapfienlem3  7644  cantnflem2  7886  r1sucg  7964  r1suc  7965  acnrcl  8200  dfac5lem4  8284  fin23lem29  8498  fin23lem30  8499  axcclem  8614  alephval2  8724  0tsk  8909  0nsr  9233  peano2nn  10321  uzssz  10867  peano2uzs  10896  uzsupss  10934  fzossnn0  11563  ltweuz  11767  fzennn  11773  ser1const  11845  expp1  11855  facnn  12036  facp1  12039  bcn0  12069  bcpasc  12080  hashfzo0  12174  ccatval2  12260  ccatass  12269  eqs1  12283  swrd00  12297  swrdid  12304  swrd0  12310  wrdeqcats1  12351  wrdeqs1cat  12352  splfv2a  12381  revccat  12389  rexuz3  12819  rexanuz2  12820  r19.2uz  12822  rexuzre  12823  cau4  12827  caubnd2  12828  climrlim2  13008  climshft2  13043  climaddc1  13095  climmulc2  13097  climsubc1  13098  climsubc2  13099  climlec2  13119  isercoll2  13129  climsup  13130  climcau  13131  caurcvg  13137  caurcvg2  13138  caucvg  13139  caucvgb  13140  iseraltlem1  13142  iseralt  13145  binomlem  13274  isumshft  13284  cvgrat  13325  3prm  13762  phicl2  13825  phibndlem  13827  dfphi2  13831  crt  13835  vdwap0  14019  prmlem1a  14116  xpscfv  14482  xpsfeq  14484  oppccofval  14637  homarcl2  14885  arwrcl  14894  pleval2i  15116  letsr  15379  gsumws1  15496  mulgpropd  15639  psgnunilem2  15980  psgnprfval  16004  gexid  16059  efgmnvl  16190  efgrcl  16191  efgsval  16207  efgs1  16211  efgs1b  16212  frgpuptinv  16247  frgpup3lem  16253  lt6abl  16350  eldprd  16459  eldprdOLD  16461  isunit  16682  isirred  16724  abvrcl  16829  islss  16937  lbsss  17079  lbssp  17081  lbsind  17082  psr1basf  17555  coe1tm  17623  cssi  17950  thlle  17963  islbs4  18102  mavmulsolcl  18203  marepvcl  18221  1marepvmarrepid  18227  mdet0pr  18244  m2detleiblem1  18271  cramerimplem1  18330  cramerlem1  18334  ptpjpre1  18985  fin1aufil  19346  lmflf  19419  tsmsfbas  19539  xpsxmetlem  19795  xpsmet  19798  metustsymOLD  19977  metustsym  19978  iscmet3lem3  20642  iscmet3lem1  20643  iscmet3lem2  20644  iscmet3  20645  rrxmvallem  20744  volsup  20878  opnmblALT  20924  itg1val  21002  mpfrcl  21369  tdeglem2  21414  ulmcaulem  21743  ulmcau  21744  ulmss  21746  pserdvlem2  21777  eff1olem  21888  logdmnrp  21970  dvlog2lem  21981  logtayl  21989  cxpcn3lem  22069  atancl  22160  atanval  22163  chp1  22389  ppiublem2  22426  lgsdir2lem2  22547  lgsdir2lem3  22548  lgsquadlem2  22578  rplogsumlem1  22617  rplogsumlem2  22618  pntlemj  22736  usgraidx2v  23133  nbgraf1olem3  23174  nbgraf1olem5  23176  gxnn0suc  23573  smgrpismgm  23641  smgrpisass  23642  mndoissmgrp  23648  mndoisexid  23649  drngoi  23716  rngoueqz  23739  vci  23748  axhcompl-zf  24222  mayete3i  24953  pj3lem1  25432  fzssnn  25896  xrge0mulc1cn  26224  elmbfmvol2  26535  fibp1  26631  rrvsum  26684  ballotlemfmpn  26724  subfacp1lem1  26914  kur14lem7  26947  divcnvlin  27245  clim2div  27250  ntrivcvg  27258  ntrivcvgtail  27261  fprodntriv  27301  fprodefsum  27331  fprodeq0  27332  iprodefisumlem  27350  iprodefisum  27351  faclimlem1  27395  predel  27490  prednn0  27509  onsucsuccmpi  28136  finixpnum  28255  volsupnfl  28277  dvasin  28321  dvacos  28322  sdclem2  28479  fdc  28482  heiborlem4  28554  heiborlem6  28556  jm2.23  29187  wepwsolem  29236  climinf  29622  stoweidlem15  29653  eldmressn  29870  afvres  29921  ndmaovrcl  29953  eldmeldmressn  29983  oprabv  30000  2wlkonot3v  30237  2spthonot3v  30238  clwwlknprop  30278  clwlkisclwwlklem2a4  30289  eleclclwwlknlem1  30333  eleclclwwlknlem2  30334  erclwwlkneqlen  30341  erclwwlknref  30342  erclwwlknsym  30343  erclwwlkntr  30344  clwlkf1clwwlk  30366  wwlkextproplem1  30403  wwlkextproplem2  30404  wwlkextproplem3  30405  frgrawopreglem4  30483  frgrawopreg  30485  lincvalsng  30656  snlindsntor  30711  lincresunit3lem2  30720  lincresunit3  30721  ldepsnlinc  30756  bnj529  31432  bnj923  31460  bnj570  31597  bnj594  31604  bnj1173  31692  bnj1256  31705  bnj1259  31706  bnj1296  31711  bnj1498  31751  bj-inftyexpidisj  32110  bj-ccinftydisj  32113  bj-elccinfty  32114