Theorem eleq2s 2884

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 2858	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 220	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

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

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 2148  ax-9 2156  ax-ext 2738

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

This theorem is used by:  elrabi  3649  optocl  5760  optoclOLD  5761  ssrel  5774  eldmeldmressn  6029  imadifssran  6207  predel  6329  fveqdmss  7080  oprabv  7483  elmpocl  7664  el2mpocsbcl  8089  bropopvvv  8094  bropfvvvv  8096  ressuppss  8188  mpoxeldm  8216  mpoxopn0yelv  8218  mpoxopxnop0  8220  tfr2a  8391  rdgseg  8418  2oconcl  8497  ecexr  8708  ectocld  8789  ecoptocl  8814  brecop2  8818  eroveu  8819  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  10575  0tsk  10758  0nsr  11082  peano2nn  12263  uzssz  12901  peano2uzs  12944  uzsupss  12982  fzssnn  13615  prednn0  13699  fzossnn0  13738  fldiv4p1lem1div2  13888  modaddid  13963  ltweuz  14017  fzennn  14024  ser1const  14114  expp1  14124  facnn  14331  facp1  14334  bcpasc  14377  hashfzo0  14487  tpfo  14557  ccatval2  14635  ccatass  14646  swrd00  14704  swrd0  14720  pfx00  14736  pfx0  14737  wrdeqs1cat  14781  splfv2a  14817  revccat  14827  rexuz3  15426  rexanuz2  15427  r19.2uz  15429  rexuzre  15430  cau4  15434  caubnd2  15435  climrlim2  15624  climshft2  15659  climaddc1  15712  climmulc2  15714  climsubc1  15715  climsubc2  15716  climlec2  15736  isercoll2  15746  climsup  15747  climcau  15748  caurcvg  15754  caurcvg2  15755  caucvg  15756  caucvgb  15757  iseraltlem1  15759  iseralt  15762  binomlem  15909  isumshft  15919  cvgrat  15963  clim2div  15969  ntrivcvg  15977  ntrivcvgtail  15980  fprodntriv  16022  fprodeq0  16055  fprodefsum  16174  pwp1fsum  16474  3prm  16777  phicl2  16852  phibndlem  16854  dfphi2  16858  crth  16862  vdwap0  17061  prmlem1a  17191  fvprif  17640  xpsfeq  17642  oppccofval  17797  homarcl2  18117  arwrcl  18126  pleval2i  18415  letsr  18674  gsumws1  18928  smndex1mndlem  19002  mulgnngsum  19176  mulgpropd  19213  psgnunilem2  19596  psgnprfval  19622  gexid  19682  efgmnvl  19815  efgrcl  19816  efgsval  19832  efgs1  19836  efgs1b  19837  frgpuptinv  19872  frgpup3lem  19878  lt6abl  19996  eldprd  20107  isunit  20488  isirred  20534  fldhmsubc  20925  abvrcl  20953  islss  21092  lbsss  21235  lbssp  21237  lbsind  21238  cssi  21871  thlle  21884  islbs4  22019  psrbagleadd1  22115  mpfrcl  22273  psr1basf  22398  coe1tm  22471  ply1frcl  22515  mavmulsolcl  22745  marepvcl  22763  1marepvmarrepid  22769  mdet0pr  22786  m2detleiblem1  22818  cramerimplem1  22877  cramerlem1  22881  chpscmat  23036  chpscmatgsumbin  23038  chpscmatgsummon  23039  ptpjpre1  23765  fin1aufil  24126  lmflf  24199  tsmsfbas  24322  xpsxmetlem  24573  xpsmet  24576  metustsym  24749  iscmet3lem3  25486  iscmet3lem1  25487  iscmet3lem2  25488  iscmet3  25489  rrxmvallem  25600  volsup  25752  opnmblALT  25799  itg1val  25879  tdeglem2  26255  ulmcaulem  26594  ulmcau  26595  ulmss  26597  pserdvlem2  26628  eff1olem  26750  logdmnrp  26843  dvlog2lem  26854  logtayl  26862  cxpcn3lem  26949  atancl  27083  atanval  27086  chp1  27368  ppiublem2  27404  lgsdir2lem2  27527  lgsdir2lem3  27528  lgsquadlem2  27582  2lgslem1b  27593  rplogsumlem1  27685  rplogsumlem2  27686  pntlemj  27804  nnne0s  28567  1vgrex  29389  edglnl  29530  usgredg2v  29614  umgrres1lem  29697  upgrres1  29700  nbupgrres  29751  clwlkwlk  30161  wwlksnextproplem1  30295  wwlksnextproplem2  30296  wwlksnextproplem3  30297  rusgrnumwwlkb0  30360  clwlkclwwlklem2a4  30385  eleclclwwlknlem1  30448  eleclclwwlknlem2  30449  erclwwlkneqlen  30456  erclwwlknref  30457  erclwwlknsym  30458  erclwwlkntr  30459  hashecclwwlkn1  30465  umgrhashecclwwlk  30466  frgrnbnb  30681  frgrwopreglem4  30703  frgrwopreglem5  30709  frgrwopreg  30711  numclwlk1  30759  vciOLD  30950  axhcompl-zf  31387  mayete3i  32117  pj3lem1  32595  fzto1stfv1  33452  fzto1st  33454  fzto1stinvn  33455  psgnfzto1st  33456  rmfsupp2  33588  erler  33616  selvply1rhmlemb  33940  vieta  34001  submat1n  34226  xrge0mulc1cn  34362  fiunelros  34596  elmbfmvol2  34689  fibp1  34823  rrvsum  34876  ballotlemfmpn  34917  reprsuc  35034  bnj529  35162  bnj923  35189  bnj570  35325  bnj594  35332  bnj1173  35422  bnj1256  35435  bnj1259  35436  bnj1296  35441  bnj1498  35481  rankfo  35530  fineqvnttrclselem1  35558  subfacp1lem1  35692  kur14lem7  35725  sat1el2xp  35892  mvrsval  36018  mvrsfpw  36019  mrsubcv  36023  mrsubccat  36031  msubff  36043  msrid  36058  msubvrs  36073  mppsval  36085  divcnvlin  36246  iprodefisumlem  36253  iprodefisum  36254  faclimlem1  36256  onsucsuccmpi  36995  bj-opelresdm  37830  bj-inftyexpitaudisj  37890  bj-inftyexpidisj  37895  bj-ccinftydisj  37898  bj-elccinfty  37899  finixpnum  38297  poimirlem5  38317  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem9  38321  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem13  38325  poimirlem14  38326  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem18  38330  poimirlem19  38331  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem29  38341  poimirlem30  38342  broucube  38346  volsupnfl  38357  dvasin  38396  dvacos  38397  sdclem2  38434  fdc  38437  heiborlem4  38506  heiborlem6  38508  smgrpismgmOLD  38554  mndoissmgrpOLD  38560  mndoisexid  38561  rngoueqz  38632  drngoi  38643  dfadjliftmap2  39147  dfblockliftmap2  39151  sucpre  39187  eldisjsim2  39625  redvmptabs  43162  mhphflem  43369  prjspertr  43378  prjsperref  43379  prjspersym  43380  prjspreln0  43382  prjspvs  43383  prjsprellsp  43384  jm2.23  43764  wepwsolem  43810  omabs2  44100  omcl3g  44102  trclfvdecomr  44495  mnuprdlem1  45023  mnuprdlem2  45024  binomcxplemdvbinom  45104  binomcxplemnotnn0  45107  orbitcl  45707  ssfiunibd  46069  climinf  46363  stoweidlem15  46770  fourierdlem66  46927  etransclem37  47026  smfsupmpt  47570  smfinfmpt  47574  smflimsuplem8  47582  eldmressn  47815  afvres  47950  ndmaovrcl  47982  2ltceilhalf  48110  minusmodnep2tmod  48137  modmknepk  48146  mod2addne  48148  modm2nep1  48150  modm1nep2  48152  modm1nem2  48153  modm1p1ne  48154  sprsymrelfv  48284  fmtnofz04prm  48370  31prm  48390  ppivalnnnprm  48421  indprmfz  48423  stgr0  48766  stgr1  48767  gpgiedgdmellem  48852  gpgvtx1  48860  gpgedgvtx1  48868  gpgedg2iv  48873  gpg5nbgrvtx13starlem2  48878  pgnbgreunbgrlem3  48924  pgnbgreunbgrlem6  48930  2zrngamnd  49053  2zrngacmnd  49054  2zrngagrp  49055  2zrngALT  49060  2zrngnmlid  49061  2zrngnmlid2  49063  fldhmsubcALTV  49139  lincvalsng  49237  snlindsntor  49292  lincresunit3lem2  49301  lincresunit3  49302  ldepsnlinc  49329  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441  rrx2pnecoorneor  49536  rrx2linest  49563  rrx2linesl  49564  isorcl  49852  catcrcl  50214  setc2othin  50285