Theorem eleq2s 2854

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  elrabi  3630  optocl  5725  optoclOLD  5726  ssrel  5739  eldmeldmressn  5990  predel  6285  fveqdmss  7030  oprabv  7427  elmpocl  7608  el2mpocsbcl  8035  bropopvvv  8040  bropfvvvv  8042  ressuppss  8133  mpoxeldm  8161  mpoxopn0yelv  8163  mpoxopxnop0  8165  tfr2a  8334  rdgseg  8361  2oconcl  8438  ecexr  8648  ectocld  8729  ecoptocl  8754  brecop2  8758  eroveu  8759  mapfvd  8827  mapsnconst  8840  mapfienlem1  9318  mapfienlem2  9319  mapfienlem3  9320  cantnflem2  9611  r1sucg  9693  r1suc  9694  acnrcl  9964  dfac5lem4  10048  dfac5lem4OLD  10050  fin23lem29  10263  fin23lem30  10264  axcclem  10379  alephval2  10495  0tsk  10678  0nsr  11002  peano2nn  12186  uzssz  12809  peano2uzs  12852  uzsupss  12890  fzssnn  13522  prednn0  13606  fzossnn0  13645  fldiv4p1lem1div2  13794  modaddid  13869  ltweuz  13923  fzennn  13930  ser1const  14020  expp1  14030  facnn  14237  facp1  14240  bcpasc  14283  hashfzo0  14392  tpfo  14462  ccatval2  14540  ccatass  14551  swrd00  14607  swrd0  14621  pfx00  14637  pfx0  14638  wrdeqs1cat  14682  splfv2a  14718  revccat  14728  rexuz3  15311  rexanuz2  15312  r19.2uz  15314  rexuzre  15315  cau4  15319  caubnd2  15320  climrlim2  15509  climshft2  15544  climaddc1  15597  climmulc2  15599  climsubc1  15600  climsubc2  15601  climlec2  15621  isercoll2  15631  climsup  15632  climcau  15633  caurcvg  15639  caurcvg2  15640  caucvg  15641  caucvgb  15642  iseraltlem1  15644  iseralt  15647  binomlem  15794  isumshft  15804  cvgrat  15848  clim2div  15854  ntrivcvg  15862  ntrivcvgtail  15865  fprodntriv  15907  fprodeq0  15940  fprodefsum  16060  pwp1fsum  16360  3prm  16663  phicl2  16738  phibndlem  16740  dfphi2  16744  crth  16748  vdwap0  16947  prmlem1a  17077  fvprif  17525  xpsfeq  17527  oppccofval  17682  homarcl2  18002  arwrcl  18011  pleval2i  18300  letsr  18559  gsumws1  18806  smndex1mndlem  18880  mulgnngsum  19055  mulgpropd  19092  psgnunilem2  19470  psgnprfval  19496  gexid  19556  efgmnvl  19689  efgrcl  19690  efgsval  19706  efgs1  19710  efgs1b  19711  frgpuptinv  19746  frgpup3lem  19752  lt6abl  19870  eldprd  19981  isunit  20353  isirred  20399  fldhmsubc  20762  abvrcl  20790  islss  20929  lbsss  21072  lbssp  21074  lbsind  21075  cssi  21664  thlle  21677  islbs4  21812  psrbagleadd1  21908  mpfrcl  22063  psr1basf  22165  coe1tm  22238  ply1frcl  22283  mavmulsolcl  22516  marepvcl  22534  1marepvmarrepid  22540  mdet0pr  22557  m2detleiblem1  22589  cramerimplem1  22648  cramerlem1  22652  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  ptpjpre1  23536  fin1aufil  23897  lmflf  23970  tsmsfbas  24093  xpsxmetlem  24344  xpsmet  24347  metustsym  24520  iscmet3lem3  25257  iscmet3lem1  25258  iscmet3lem2  25259  iscmet3  25260  rrxmvallem  25371  volsup  25523  opnmblALT  25570  itg1val  25650  tdeglem2  26026  ulmcaulem  26359  ulmcau  26360  ulmss  26362  pserdvlem2  26393  eff1olem  26512  logdmnrp  26605  dvlog2lem  26616  logtayl  26624  cxpcn3lem  26711  atancl  26845  atanval  26848  chp1  27130  ppiublem2  27166  lgsdir2lem2  27289  lgsdir2lem3  27290  lgsquadlem2  27344  2lgslem1b  27355  rplogsumlem1  27447  rplogsumlem2  27448  pntlemj  27566  nnne0s  28329  1vgrex  29071  edglnl  29212  usgredg2v  29296  umgrres1lem  29379  upgrres1  29382  nbupgrres  29433  clwlkwlk  29843  wwlksnextproplem1  29977  wwlksnextproplem2  29978  wwlksnextproplem3  29979  rusgrnumwwlkb0  30042  clwlkclwwlklem2a4  30067  eleclclwwlknlem1  30130  eleclclwwlknlem2  30131  erclwwlkneqlen  30138  erclwwlknref  30139  erclwwlknsym  30140  erclwwlkntr  30141  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  frgrnbnb  30363  frgrwopreglem4  30385  frgrwopreglem5  30391  frgrwopreg  30393  numclwlk1  30441  vciOLD  30632  axhcompl-zf  31069  mayete3i  31799  pj3lem1  32277  fzto1stfv1  33162  fzto1st  33164  fzto1stinvn  33165  psgnfzto1st  33166  rmfsupp2  33299  erler  33326  vieta  33724  submat1n  33949  xrge0mulc1cn  34085  fiunelros  34318  elmbfmvol2  34411  fibp1  34545  rrvsum  34598  ballotlemfmpn  34639  reprsuc  34759  bnj529  34884  bnj923  34911  bnj570  35047  bnj594  35054  bnj1173  35144  bnj1256  35157  bnj1259  35158  bnj1296  35163  bnj1498  35203  fineqvnttrclselem1  35265  subfacp1lem1  35361  kur14lem7  35394  sat1el2xp  35561  mvrsval  35687  mvrsfpw  35688  mrsubcv  35692  mrsubccat  35700  msubff  35712  msrid  35727  msubvrs  35742  mppsval  35754  divcnvlin  35915  iprodefisumlem  35922  iprodefisum  35923  faclimlem1  35925  onsucsuccmpi  36625  bj-opelresdm  37459  bj-inftyexpitaudisj  37519  bj-inftyexpidisj  37524  bj-ccinftydisj  37527  bj-elccinfty  37528  finixpnum  37926  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem29  37970  poimirlem30  37971  broucube  37975  volsupnfl  37986  dvasin  38025  dvacos  38026  sdclem2  38063  fdc  38066  heiborlem4  38135  heiborlem6  38137  smgrpismgmOLD  38183  mndoissmgrpOLD  38189  mndoisexid  38190  rngoueqz  38261  drngoi  38272  dfadjliftmap2  38778  dfblockliftmap2  38782  sucpre  38818  eldisjsim2  39256  redvmptabs  42792  mhphflem  43029  prjspertr  43038  prjsperref  43039  prjspersym  43040  prjspreln0  43042  prjspvs  43043  prjsprellsp  43044  jm2.23  43424  wepwsolem  43470  omabs2  43760  omcl3g  43762  trclfvdecomr  44155  mnuprdlem1  44699  mnuprdlem2  44700  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  orbitcl  45384  ssfiunibd  45742  climinf  46036  stoweidlem15  46443  fourierdlem66  46600  etransclem37  46699  smfsupmpt  47243  smfinfmpt  47247  smflimsuplem8  47255  eldmressn  47485  afvres  47620  ndmaovrcl  47652  2ltceilhalf  47780  minusmodnep2tmod  47807  modmknepk  47816  mod2addne  47818  modm2nep1  47820  modm1nep2  47822  modm1nem2  47823  modm1p1ne  47824  sprsymrelfv  47954  fmtnofz04prm  48040  31prm  48060  ppivalnnnprm  48091  indprmfz  48093  stgr0  48436  stgr1  48437  gpgiedgdmellem  48522  gpgvtx1  48530  gpgedgvtx1  48538  gpgedg2iv  48543  gpg5nbgrvtx13starlem2  48548  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  2zrngamnd  48723  2zrngacmnd  48724  2zrngagrp  48725  2zrngALT  48730  2zrngnmlid  48731  2zrngnmlid2  48733  fldhmsubcALTV  48809  lincvalsng  48892  snlindsntor  48947  lincresunit3lem2  48956  lincresunit3  48957  ldepsnlinc  48984  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  rrx2pnecoorneor  49191  rrx2linest  49218  rrx2linesl  49219  isorcl  49508  catcrcl  49870  setc2othin  49941