Theorem eleq2s 2851

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  elrabi  3639  optocl  5713  optoclOLD  5714  ssrel  5727  eldmeldmressn  5978  predel  6273  fveqdmss  7017  oprabv  7412  elmpocl  7593  el2mpocsbcl  8021  bropopvvv  8026  bropfvvvv  8028  ressuppss  8119  mpoxeldm  8147  mpoxopn0yelv  8149  mpoxopxnop0  8151  tfr2a  8320  rdgseg  8347  2oconcl  8424  ecexr  8633  ectocld  8712  ecoptocl  8737  brecop2  8741  eroveu  8742  mapfvd  8809  mapsnconst  8822  mapfienlem1  9296  mapfienlem2  9297  mapfienlem3  9298  cantnflem2  9587  r1sucg  9669  r1suc  9670  acnrcl  9940  dfac5lem4  10024  dfac5lem4OLD  10026  fin23lem29  10239  fin23lem30  10240  axcclem  10355  alephval2  10470  0tsk  10653  0nsr  10977  peano2nn  12144  uzssz  12759  peano2uzs  12802  uzsupss  12840  fzssnn  13470  prednn0  13554  fzossnn0  13592  fldiv4p1lem1div2  13741  modaddid  13816  ltweuz  13870  fzennn  13877  ser1const  13967  expp1  13977  facnn  14184  facp1  14187  bcpasc  14230  hashfzo0  14339  tpfo  14409  ccatval2  14487  ccatass  14498  swrd00  14554  swrd0  14568  pfx00  14584  pfx0  14585  wrdeqs1cat  14629  splfv2a  14665  revccat  14675  rexuz3  15258  rexanuz2  15259  r19.2uz  15261  rexuzre  15262  cau4  15266  caubnd2  15267  climrlim2  15456  climshft2  15491  climaddc1  15544  climmulc2  15546  climsubc1  15547  climsubc2  15548  climlec2  15568  isercoll2  15578  climsup  15579  climcau  15580  caurcvg  15586  caurcvg2  15587  caucvg  15588  caucvgb  15589  iseraltlem1  15591  iseralt  15594  binomlem  15738  isumshft  15748  cvgrat  15792  clim2div  15798  ntrivcvg  15806  ntrivcvgtail  15809  fprodntriv  15851  fprodeq0  15884  fprodefsum  16004  pwp1fsum  16304  3prm  16607  phicl2  16681  phibndlem  16683  dfphi2  16687  crth  16691  vdwap0  16890  prmlem1a  17020  fvprif  17467  xpsfeq  17469  oppccofval  17624  homarcl2  17944  arwrcl  17953  pleval2i  18242  letsr  18501  gsumws1  18748  smndex1mndlem  18819  mulgnngsum  18994  mulgpropd  19031  psgnunilem2  19409  psgnprfval  19435  gexid  19495  efgmnvl  19628  efgrcl  19629  efgsval  19645  efgs1  19649  efgs1b  19650  frgpuptinv  19685  frgpup3lem  19691  lt6abl  19809  eldprd  19920  isunit  20293  isirred  20339  fldhmsubc  20702  abvrcl  20730  islss  20869  lbsss  21013  lbssp  21015  lbsind  21016  cssi  21623  thlle  21636  islbs4  21771  psrbagleadd1  21867  mpfrcl  22021  psr1basf  22115  coe1tm  22188  ply1frcl  22234  mavmulsolcl  22467  marepvcl  22485  1marepvmarrepid  22491  mdet0pr  22508  m2detleiblem1  22540  cramerimplem1  22599  cramerlem1  22603  chpscmat  22758  chpscmatgsumbin  22760  chpscmatgsummon  22761  ptpjpre1  23487  fin1aufil  23848  lmflf  23921  tsmsfbas  24044  xpsxmetlem  24295  xpsmet  24298  metustsym  24471  iscmet3lem3  25218  iscmet3lem1  25219  iscmet3lem2  25220  iscmet3  25221  rrxmvallem  25332  volsup  25485  opnmblALT  25532  itg1val  25612  tdeglem2  25994  ulmcaulem  26331  ulmcau  26332  ulmss  26334  pserdvlem2  26366  eff1olem  26485  logdmnrp  26578  dvlog2lem  26589  logtayl  26597  cxpcn3lem  26685  atancl  26819  atanval  26822  chp1  27105  ppiublem2  27142  lgsdir2lem2  27265  lgsdir2lem3  27266  lgsquadlem2  27320  2lgslem1b  27331  rplogsumlem1  27423  rplogsumlem2  27424  pntlemj  27542  nnne0s  28266  1vgrex  28982  edglnl  29123  usgredg2v  29207  umgrres1lem  29290  upgrres1  29293  nbupgrres  29344  clwlkwlk  29755  wwlksnextproplem1  29889  wwlksnextproplem2  29890  wwlksnextproplem3  29891  rusgrnumwwlkb0  29954  clwlkclwwlklem2a4  29979  eleclclwwlknlem1  30042  eleclclwwlknlem2  30043  erclwwlkneqlen  30050  erclwwlknref  30051  erclwwlknsym  30052  erclwwlkntr  30053  hashecclwwlkn1  30059  umgrhashecclwwlk  30060  frgrnbnb  30275  frgrwopreglem4  30297  frgrwopreglem5  30303  frgrwopreg  30305  numclwlk1  30353  vciOLD  30543  axhcompl-zf  30980  mayete3i  31710  pj3lem1  32188  fzto1stfv1  33077  fzto1st  33079  fzto1stinvn  33080  psgnfzto1st  33081  rmfsupp2  33212  erler  33239  submat1n  33839  xrge0mulc1cn  33975  fiunelros  34208  elmbfmvol2  34301  fibp1  34435  rrvsum  34488  ballotlemfmpn  34529  reprsuc  34649  bnj529  34774  bnj923  34801  bnj570  34938  bnj594  34945  bnj1173  35035  bnj1256  35048  bnj1259  35049  bnj1296  35054  bnj1498  35094  fineqvnttrclselem1  35162  subfacp1lem1  35244  kur14lem7  35277  sat1el2xp  35444  mvrsval  35570  mvrsfpw  35571  mrsubcv  35575  mrsubccat  35583  msubff  35595  msrid  35610  msubvrs  35625  mppsval  35637  divcnvlin  35798  iprodefisumlem  35805  iprodefisum  35806  faclimlem1  35808  onsucsuccmpi  36508  bj-opelresdm  37210  bj-inftyexpitaudisj  37270  bj-inftyexpidisj  37275  bj-ccinftydisj  37278  bj-elccinfty  37279  finixpnum  37665  poimirlem5  37685  poimirlem6  37686  poimirlem7  37687  poimirlem8  37688  poimirlem9  37689  poimirlem10  37690  poimirlem11  37691  poimirlem12  37692  poimirlem13  37693  poimirlem14  37694  poimirlem15  37695  poimirlem16  37696  poimirlem17  37697  poimirlem18  37698  poimirlem19  37699  poimirlem20  37700  poimirlem21  37701  poimirlem22  37702  poimirlem29  37709  poimirlem30  37710  broucube  37714  volsupnfl  37725  dvasin  37764  dvacos  37765  sdclem2  37802  fdc  37805  heiborlem4  37874  heiborlem6  37876  smgrpismgmOLD  37922  mndoissmgrpOLD  37928  mndoisexid  37929  rngoueqz  38000  drngoi  38011  dfadjliftmap2  38491  dfblockliftmap2  38494  sucpre  38529  redvmptabs  42478  mhphflem  42714  prjspertr  42723  prjsperref  42724  prjspersym  42725  prjspreln0  42727  prjspvs  42728  prjsprellsp  42729  jm2.23  43113  wepwsolem  43159  omabs2  43449  omcl3g  43451  trclfvdecomr  43845  mnuprdlem1  44389  mnuprdlem2  44390  binomcxplemdvbinom  44470  binomcxplemnotnn0  44473  orbitcl  45074  ssfiunibd  45434  climinf  45730  stoweidlem15  46137  fourierdlem66  46294  etransclem37  46393  smfsupmpt  46937  smfinfmpt  46941  smflimsuplem8  46949  eldmressn  47161  afvres  47296  ndmaovrcl  47328  2ltceilhalf  47452  minusmodnep2tmod  47477  modmknepk  47486  mod2addne  47488  modm2nep1  47490  modm1nep2  47492  modm1nem2  47493  modm1p1ne  47494  sprsymrelfv  47618  fmtnofz04prm  47701  31prm  47721  stgr0  48084  stgr1  48085  gpgiedgdmellem  48170  gpgvtx1  48178  gpgedgvtx1  48186  gpgedg2iv  48191  gpg5nbgrvtx13starlem2  48196  pgnbgreunbgrlem3  48242  pgnbgreunbgrlem6  48248  2zrngamnd  48371  2zrngacmnd  48372  2zrngagrp  48373  2zrngALT  48378  2zrngnmlid  48379  2zrngnmlid2  48381  fldhmsubcALTV  48457  lincvalsng  48541  snlindsntor  48596  lincresunit3lem2  48605  lincresunit3  48606  ldepsnlinc  48633  nn0sumshdiglemA  48744  nn0sumshdiglemB  48745  rrx2pnecoorneor  48840  rrx2linest  48867  rrx2linesl  48868  isorcl  49158  catcrcl  49520  setc2othin  49591