Theorem eleq2s 2562

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 2532	. 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 1398   e. wcel 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449

This theorem is referenced by:  elrabi  3251  epelg  4781  elxpi  5004  optocl  5065  eldmeldmressn  5302  fveqdmss  6002  oprabv  6318  elmpt2cl  6490  bropopvvv  6853  ressuppss  6911  mpt2xopn0yelv  6933  mpt2xopxnop0  6935  tfr2a  7056  rdgseg  7080  2oconcl  7145  ecexr  7308  ectocld  7370  ecoptocl  7393  brecop2  7397  eroveu  7398  mapsnconst  7457  mapfienlem1  7856  mapfienlem2  7857  mapfienlem3  7858  cantnflem2  8100  r1sucg  8178  r1suc  8179  acnrcl  8414  dfac5lem4  8498  fin23lem29  8712  fin23lem30  8713  axcclem  8828  alephval2  8938  0tsk  9122  0nsr  9445  peano2nn  10543  uzssz  11101  peano2uzs  11136  uzsupss  11175  fzossnn0  11833  ltweuz  12054  fzennn  12060  ser1const  12145  expp1  12155  facnn  12337  facp1  12340  bcpasc  12381  hashfzo0  12472  ccatval2  12585  ccatass  12594  swrd00  12634  swrd0  12650  wrdeqs1cat  12691  splfv2a  12723  revccat  12731  rexuz3  13263  rexanuz2  13264  r19.2uz  13266  rexuzre  13267  cau4  13271  caubnd2  13272  climrlim2  13452  climshft2  13487  climaddc1  13539  climmulc2  13541  climsubc1  13542  climsubc2  13543  climlec2  13563  isercoll2  13573  climsup  13574  climcau  13575  caurcvg  13581  caurcvg2  13582  caucvg  13583  caucvgb  13584  iseraltlem1  13586  iseralt  13589  binomlem  13723  isumshft  13733  cvgrat  13774  clim2div  13780  ntrivcvg  13788  ntrivcvgtail  13791  fprodntriv  13831  fprodeq0  13861  fprodefsum  13912  3prm  14318  phicl2  14382  phibndlem  14384  dfphi2  14388  crt  14392  vdwap0  14578  prmlem1a  14676  xpscfv  15051  xpsfeq  15053  oppccofval  15204  homarcl2  15513  arwrcl  15522  pleval2i  15793  letsr  16056  gsumws1  16206  mulgpropd  16374  psgnunilem2  16719  psgnprfval  16745  gexid  16800  efgmnvl  16931  efgrcl  16932  efgsval  16948  efgs1  16952  efgs1b  16953  frgpuptinv  16988  frgpup3lem  16994  lt6abl  17096  eldprd  17230  eldprdOLD  17232  isunit  17501  isirred  17543  abvrcl  17665  islss  17776  lbsss  17918  lbssp  17920  lbsind  17921  mpfrcl  18382  psr1basf  18435  coe1tm  18509  ply1frcl  18550  cssi  18888  thlle  18901  islbs4  19034  mavmulsolcl  19220  marepvcl  19238  1marepvmarrepid  19244  mdet0pr  19261  m2detleiblem1  19293  cramerimplem1  19352  cramerlem1  19356  chpscmat  19510  chpscmatgsumbin  19512  chpscmatgsummon  19513  ptpjpre1  20238  fin1aufil  20599  lmflf  20672  tsmsfbas  20792  xpsxmetlem  21048  xpsmet  21051  metustsymOLD  21230  metustsym  21231  iscmet3lem3  21895  iscmet3lem1  21896  iscmet3lem2  21897  iscmet3  21898  rrxmvallem  21997  volsup  22132  opnmblALT  22178  itg1val  22256  tdeglem2  22625  ulmcaulem  22955  ulmcau  22956  ulmss  22958  pserdvlem2  22989  eff1olem  23101  logdmnrp  23190  dvlog2lem  23201  logtayl  23209  cxpcn3lem  23289  atancl  23409  atanval  23412  chp1  23639  ppiublem2  23676  lgsdir2lem2  23797  lgsdir2lem3  23798  lgsquadlem2  23828  rplogsumlem1  23867  rplogsumlem2  23868  pntlemj  23986  uhgrac  24507  usgraidx2v  24595  nbgraf1olem3  24645  nbgraf1olem5  24647  wwlkextproplem1  24943  wwlkextproplem2  24944  wwlkextproplem3  24945  clwwlknprop  24974  clwlkisclwwlklem2a4  24986  eleclclwwlknlem1  25019  eleclclwwlknlem2  25020  erclwwlkneqlen  25026  erclwwlknref  25027  erclwwlknsym  25028  erclwwlkntr  25029  clwlkf1clwwlk  25052  2wlkonot3v  25077  2spthonot3v  25078  frgrawopreglem4  25249  frgrawopreg  25251  gxnn0suc  25464  smgrpismgmOLD  25532  smgrpisass  25533  mndoissmgrpOLD  25539  mndoisexid  25540  drngoi  25607  rngoueqz  25630  vci  25639  axhcompl-zf  26113  mayete3i  26844  pj3lem1  27323  fzssnn  27829  xrge0mulc1cn  28158  elmbfmvol2  28475  fibp1  28604  rrvsum  28657  ballotlemfmpn  28697  subfacp1lem1  28887  kur14lem7  28920  mvrsval  29129  mvrsfpw  29130  mrsubcv  29134  mrsubccat  29142  msubff  29154  msrid  29169  msubvrs  29184  mppsval  29196  divcnvlin  29359  iprodefisumlem  29364  iprodefisum  29365  faclimlem1  29409  predel  29503  prednn0  29522  onsucsuccmpi  30136  finixpnum  30278  volsupnfl  30299  dvasin  30343  dvacos  30344  sdclem2  30475  fdc  30478  heiborlem4  30550  heiborlem6  30552  jm2.23  31177  wepwsolem  31226  binomcxplemdvbinom  31499  binomcxplemnotnn0  31502  ssfiunibd  31748  climinf  31851  stoweidlem15  32036  fourierdlem66  32194  etransclem37  32293  eldmressn  32447  afvres  32496  ndmaovrcl  32528  pfx00  32612  pfx0  32613  usgresvm1  32815  usgresvm1ALT  32819  2zrngamnd  33001  2zrngacmnd  33002  2zrngagrp  33003  2zrngALT  33008  2zrngnmlid  33009  2zrngnmlid2  33011  fldhmsubc  33146  fldhmsubcALTV  33165  lincvalsng  33271  snlindsntor  33326  lincresunit3lem2  33335  lincresunit3  33336  ldepsnlinc  33363  nn0sumshdiglemA  33494  nn0sumshdiglemB  33495  bnj529  34199  bnj923  34227  bnj570  34364  bnj594  34371  bnj1173  34459  bnj1256  34472  bnj1259  34473  bnj1296  34478  bnj1498  34518  bj-inftyexpidisj  35013  bj-ccinftydisj  35016  bj-elccinfty  35017