Theorem eleq2s 2878

Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
eleq2s.1	⊢ (𝐴 ∈ 𝐵 → 𝜑)
eleq2s.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleq2s	⊢ (𝐴 ∈ 𝐶 → 𝜑)

Proof of Theorem eleq2s

Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3 ⊢ 𝐶 = 𝐵
2	1	eleq2i 2852	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 220	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  elrabi  3641  optocl  5749  optoclOLD  5750  ssrel  5763  eldmeldmressn  6018  imadifssran  6197  predel  6319  fveqdmss  7071  oprabv  7473  elmpocl  7655  el2mpocsbcl  8082  bropopvvv  8087  bropfvvvv  8089  ressuppss  8181  mpoxeldm  8209  mpoxopn0yelv  8211  mpoxopxnop0  8213  tfr2a  8384  rdgseg  8411  2oconcl  8490  ecexr  8701  ectocld  8782  ecoptocl  8807  brecop2  8811  eroveu  8812  mapfvd  8886  mapsnconst  8899  mapfienlem1  9375  mapfienlem2  9376  mapfienlem3  9377  cantnflem2  9669  r1sucg  9751  r1suc  9752  karden  9898  acnrcl  10045  dfac5lem4  10129  fin23lem29  10343  fin23lem30  10344  axcclem  10459  alephval2  10581  0tsk  10764  0nsr  11088  peano2nn  12269  uzssz  12908  peano2uzs  12951  uzsupss  12989  fzssnn  13623  prednn0  13707  fzossnn0  13746  fldiv4p1lem1div2  13896  modaddid  13971  ltweuz  14025  fzennn  14032  ser1const  14122  expp1  14132  facnn  14339  facp1  14342  bcpasc  14385  hashfzo0  14495  tpfo  14565  ccatval2  14643  ccatass  14654  swrd00  14712  swrd0  14728  pfx00  14744  pfx0  14745  wrdeqs1cat  14789  splfv2a  14825  revccat  14835  rexuz3  15436  rexanuz2  15437  r19.2uz  15439  rexuzre  15440  cau4  15444  caubnd2  15445  climrlim2  15634  climshft2  15669  climaddc1  15722  climmulc2  15724  climsubc1  15725  climsubc2  15726  climlec2  15746  isercoll2  15756  climsup  15757  climcau  15758  caurcvg  15764  caurcvg2  15765  caucvg  15766  caucvgb  15767  iseraltlem1  15769  iseralt  15772  binomlem  15918  isumshft  15928  cvgrat  15972  clim2div  15978  ntrivcvg  15986  ntrivcvgtail  15989  fprodntriv  16029  fprodeq0  16062  fprodefsum  16181  pwp1fsum  16481  3prm  16784  phicl2  16859  phibndlem  16861  dfphi2  16865  crth  16869  vdwap0  17068  prmlem1a  17198  fvprif  17647  xpsfeq  17649  oppccofval  17804  homarcl2  18124  arwrcl  18133  pleval2i  18422  letsr  18681  gsumws1  18947  smndex1mndlem  19021  mulgnngsum  19202  mulgpropd  19239  psgnunilem2  19622  psgnprfval  19648  gexid  19708  efgmnvl  19841  efgrcl  19842  efgsval  19858  efgs1  19862  efgs1b  19863  frgpuptinv  19898  frgpup3lem  19904  lt6abl  20022  eldprd  20133  isunit  20514  isirred  20560  fldhmsubc  20951  abvrcl  20979  islss  21118  lbsss  21261  lbssp  21263  lbsind  21264  cssi  21897  thlle  21910  islbs4  22045  psrbagleadd1  22143  mpfrcl  22301  psr1basf  22426  coe1tm  22499  ply1frcl  22543  mavmulsolcl  22773  marepvcl  22791  1marepvmarrepid  22797  mdet0pr  22814  m2detleiblem1  22846  cramerimplem1  22908  cramerlem1  22912  chpscmat  23067  chpscmatgsumbin  23069  chpscmatgsummon  23070  ptpjpre1  23797  fin1aufil  24158  lmflf  24231  tsmsfbas  24354  xpsxmetlem  24605  xpsmet  24608  metustsym  24781  iscmet3lem3  25518  iscmet3lem1  25519  iscmet3lem2  25520  iscmet3  25521  rrxmvallem  25632  volsup  25784  opnmblALT  25831  itg1val  25911  tdeglem2  26286  ulmcaulem  26630  ulmcau  26631  ulmss  26633  pserdvlem2  26664  eff1olem  26785  logdmnrp  26878  dvlog2lem  26889  logtayl  26897  cxpcn3lem  26984  atancl  27118  atanval  27121  chp1  27403  ppiublem2  27439  lgsdir2lem2  27562  lgsdir2lem3  27563  lgsquadlem2  27617  2lgslem1b  27628  rplogsumlem1  27720  rplogsumlem2  27721  pntlemj  27839  nnne0s  28602  1vgrex  29459  edglnl  29600  usgredg2v  29687  umgrres1lem  29770  upgrres1  29773  nbupgrres  29824  clwlkwlk  30241  wwlksnextproplem1  30377  wwlksnextproplem2  30378  wwlksnextproplem3  30379  rusgrnumwwlkb0  30442  clwlkclwwlklem2a4  30467  eleclclwwlknlem1  30530  eleclclwwlknlem2  30531  erclwwlkneqlen  30538  erclwwlknref  30539  erclwwlknsym  30540  erclwwlkntr  30541  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  frgrnbnb  30773  frgrwopreglem4  30795  frgrwopreglem5  30801  frgrwopreg  30803  numclwlk1  30851  vciOLD  31042  axhcompl-zf  31479  mayete3i  32209  pj3lem1  32687  fzto1stfv1  33541  fzto1st  33543  fzto1stinvn  33544  psgnfzto1st  33545  rmfsupp2  33677  erler  33705  selvply1rhmlemb  34029  vieta  34090  submat1n  34315  xrge0mulc1cn  34451  fiunelros  34685  elmbfmvol2  34778  fibp1  34912  rrvsum  34965  ballotlemfmpn  35006  reprsuc  35123  bnj529  35251  bnj923  35278  bnj570  35414  bnj594  35421  bnj1173  35511  bnj1256  35524  bnj1259  35525  bnj1296  35530  bnj1498  35570  rankfo  35619  fineqvnttrclselem1  35647  subfacp1lem1  35758  kur14lem7  35791  sat1el2xp  35958  mvrsval  36084  mvrsfpw  36085  mrsubcv  36089  mrsubccat  36097  msubff  36109  msrid  36124  msubvrs  36139  mppsval  36151  divcnvlin  36312  iprodefisumlem  36319  iprodefisum  36320  faclimlem1  36322  onsucsuccmpi  37062  bj-opelresdm  37897  bj-inftyexpitaudisj  37957  bj-inftyexpidisj  37962  bj-ccinftydisj  37965  bj-elccinfty  37966  finixpnum  38359  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem9  38378  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem29  38398  poimirlem30  38399  broucube  38403  volsupnfl  38414  dvasin  38453  dvacos  38454  sdclem2  38492  fdc  38495  heiborlem4  38564  heiborlem6  38566  smgrpismgmOLD  38612  mndoissmgrpOLD  38618  mndoisexid  38619  rngoueqz  38690  drngoi  38701  dfadjliftmap2  39205  dfblockliftmap2  39209  sucpre  39245  eldisjsim2  39683  redvmptabs  43235  mhphflem  43442  prjspertr  43451  prjsperref  43452  prjspersym  43453  prjspreln0  43455  prjspvs  43456  prjsprellsp  43457  jm2.23  43837  wepwsolem  43883  omabs2  44173  omcl3g  44175  trclfvdecomr  44568  mnuprdlem1  45096  mnuprdlem2  45097  binomcxplemdvbinom  45177  binomcxplemnotnn0  45180  orbitcl  45780  ssfiunibd  46142  climinf  46436  stoweidlem15  46843  fourierdlem66  47000  etransclem37  47099  smfsupmpt  47643  smfinfmpt  47647  smflimsuplem8  47655  eldmressn  47925  afvres  48060  ndmaovrcl  48092  2ltceilhalf  48220  minusmodnep2tmod  48247  modmknepk  48256  mod2addne  48258  modm2nep1  48260  modm1nep2  48262  modm1nem2  48263  modm1p1ne  48264  sprsymrelfv  48394  fmtnofz04prm  48480  31prm  48500  ppivalnnnprm  48531  indprmfz  48533  stgr0  48876  stgr1  48877  gpgiedgdmellem  48962  gpgvtx1  48970  gpgedgvtx1  48978  gpgedg2iv  48983  gpg5nbgrvtx13starlem2  48988  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  2zrngamnd  49162  2zrngacmnd  49163  2zrngagrp  49164  2zrngALT  49169  2zrngnmlid  49170  2zrngnmlid2  49172  fldhmsubcALTV  49248  lincvalsng  49346  snlindsntor  49401  lincresunit3lem2  49410  lincresunit3  49411  ldepsnlinc  49438  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  rrx2pnecoorneor  49645  rrx2linest  49672  rrx2linesl  49673  isorcl  49959  catcrcl  50321  setc2othin  50392