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 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 2708

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

This theorem is referenced by:  elrabi  3642  optocl  5718  optoclOLD  5719  ssrel  5732  eldmeldmressn  5984  predel  6279  fveqdmss  7023  oprabv  7418  elmpocl  7599  el2mpocsbcl  8027  bropopvvv  8032  bropfvvvv  8034  ressuppss  8125  mpoxeldm  8153  mpoxopn0yelv  8155  mpoxopxnop0  8157  tfr2a  8326  rdgseg  8353  2oconcl  8430  ecexr  8640  ectocld  8719  ecoptocl  8744  brecop2  8748  eroveu  8749  mapfvd  8817  mapsnconst  8830  mapfienlem1  9308  mapfienlem2  9309  mapfienlem3  9310  cantnflem2  9599  r1sucg  9681  r1suc  9682  acnrcl  9952  dfac5lem4  10036  dfac5lem4OLD  10038  fin23lem29  10251  fin23lem30  10252  axcclem  10367  alephval2  10483  0tsk  10666  0nsr  10990  peano2nn  12157  uzssz  12772  peano2uzs  12815  uzsupss  12853  fzssnn  13484  prednn0  13568  fzossnn0  13606  fldiv4p1lem1div2  13755  modaddid  13830  ltweuz  13884  fzennn  13891  ser1const  13981  expp1  13991  facnn  14198  facp1  14201  bcpasc  14244  hashfzo0  14353  tpfo  14423  ccatval2  14501  ccatass  14512  swrd00  14568  swrd0  14582  pfx00  14598  pfx0  14599  wrdeqs1cat  14643  splfv2a  14679  revccat  14689  rexuz3  15272  rexanuz2  15273  r19.2uz  15275  rexuzre  15276  cau4  15280  caubnd2  15281  climrlim2  15470  climshft2  15505  climaddc1  15558  climmulc2  15560  climsubc1  15561  climsubc2  15562  climlec2  15582  isercoll2  15592  climsup  15593  climcau  15594  caurcvg  15600  caurcvg2  15601  caucvg  15602  caucvgb  15603  iseraltlem1  15605  iseralt  15608  binomlem  15752  isumshft  15762  cvgrat  15806  clim2div  15812  ntrivcvg  15820  ntrivcvgtail  15823  fprodntriv  15865  fprodeq0  15898  fprodefsum  16018  pwp1fsum  16318  3prm  16621  phicl2  16695  phibndlem  16697  dfphi2  16701  crth  16705  vdwap0  16904  prmlem1a  17034  fvprif  17482  xpsfeq  17484  oppccofval  17639  homarcl2  17959  arwrcl  17968  pleval2i  18257  letsr  18516  gsumws1  18763  smndex1mndlem  18834  mulgnngsum  19009  mulgpropd  19046  psgnunilem2  19424  psgnprfval  19450  gexid  19510  efgmnvl  19643  efgrcl  19644  efgsval  19660  efgs1  19664  efgs1b  19665  frgpuptinv  19700  frgpup3lem  19706  lt6abl  19824  eldprd  19935  isunit  20309  isirred  20355  fldhmsubc  20718  abvrcl  20746  islss  20885  lbsss  21029  lbssp  21031  lbsind  21032  cssi  21639  thlle  21652  islbs4  21787  psrbagleadd1  21884  mpfrcl  22040  psr1basf  22142  coe1tm  22215  ply1frcl  22262  mavmulsolcl  22495  marepvcl  22513  1marepvmarrepid  22519  mdet0pr  22536  m2detleiblem1  22568  cramerimplem1  22627  cramerlem1  22631  chpscmat  22786  chpscmatgsumbin  22788  chpscmatgsummon  22789  ptpjpre1  23515  fin1aufil  23876  lmflf  23949  tsmsfbas  24072  xpsxmetlem  24323  xpsmet  24326  metustsym  24499  iscmet3lem3  25246  iscmet3lem1  25247  iscmet3lem2  25248  iscmet3  25249  rrxmvallem  25360  volsup  25513  opnmblALT  25560  itg1val  25640  tdeglem2  26022  ulmcaulem  26359  ulmcau  26360  ulmss  26362  pserdvlem2  26394  eff1olem  26513  logdmnrp  26606  dvlog2lem  26617  logtayl  26625  cxpcn3lem  26713  atancl  26847  atanval  26850  chp1  27133  ppiublem2  27170  lgsdir2lem2  27293  lgsdir2lem3  27294  lgsquadlem2  27348  2lgslem1b  27359  rplogsumlem1  27451  rplogsumlem2  27452  pntlemj  27570  nnne0s  28333  1vgrex  29075  edglnl  29216  usgredg2v  29300  umgrres1lem  29383  upgrres1  29386  nbupgrres  29437  clwlkwlk  29848  wwlksnextproplem1  29982  wwlksnextproplem2  29983  wwlksnextproplem3  29984  rusgrnumwwlkb0  30047  clwlkclwwlklem2a4  30072  eleclclwwlknlem1  30135  eleclclwwlknlem2  30136  erclwwlkneqlen  30143  erclwwlknref  30144  erclwwlknsym  30145  erclwwlkntr  30146  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  frgrnbnb  30368  frgrwopreglem4  30390  frgrwopreglem5  30396  frgrwopreg  30398  numclwlk1  30446  vciOLD  30636  axhcompl-zf  31073  mayete3i  31803  pj3lem1  32281  fzto1stfv1  33183  fzto1st  33185  fzto1stinvn  33186  psgnfzto1st  33187  rmfsupp2  33320  erler  33347  vieta  33736  submat1n  33962  xrge0mulc1cn  34098  fiunelros  34331  elmbfmvol2  34424  fibp1  34558  rrvsum  34611  ballotlemfmpn  34652  reprsuc  34772  bnj529  34897  bnj923  34924  bnj570  35061  bnj594  35068  bnj1173  35158  bnj1256  35171  bnj1259  35172  bnj1296  35177  bnj1498  35217  fineqvnttrclselem1  35277  subfacp1lem1  35373  kur14lem7  35406  sat1el2xp  35573  mvrsval  35699  mvrsfpw  35700  mrsubcv  35704  mrsubccat  35712  msubff  35724  msrid  35739  msubvrs  35754  mppsval  35766  divcnvlin  35927  iprodefisumlem  35934  iprodefisum  35935  faclimlem1  35937  onsucsuccmpi  36637  bj-opelresdm  37346  bj-inftyexpitaudisj  37406  bj-inftyexpidisj  37411  bj-ccinftydisj  37414  bj-elccinfty  37415  finixpnum  37802  poimirlem5  37822  poimirlem6  37823  poimirlem7  37824  poimirlem8  37825  poimirlem9  37826  poimirlem10  37827  poimirlem11  37828  poimirlem12  37829  poimirlem13  37830  poimirlem14  37831  poimirlem15  37832  poimirlem16  37833  poimirlem17  37834  poimirlem18  37835  poimirlem19  37836  poimirlem20  37837  poimirlem21  37838  poimirlem22  37839  poimirlem29  37846  poimirlem30  37847  broucube  37851  volsupnfl  37862  dvasin  37901  dvacos  37902  sdclem2  37939  fdc  37942  heiborlem4  38011  heiborlem6  38013  smgrpismgmOLD  38059  mndoissmgrpOLD  38065  mndoisexid  38066  rngoueqz  38137  drngoi  38148  dfadjliftmap2  38628  dfblockliftmap2  38631  sucpre  38666  redvmptabs  42611  mhphflem  42835  prjspertr  42844  prjsperref  42845  prjspersym  42846  prjspreln0  42848  prjspvs  42849  prjsprellsp  42850  jm2.23  43234  wepwsolem  43280  omabs2  43570  omcl3g  43572  trclfvdecomr  43965  mnuprdlem1  44509  mnuprdlem2  44510  binomcxplemdvbinom  44590  binomcxplemnotnn0  44593  orbitcl  45194  ssfiunibd  45553  climinf  45848  stoweidlem15  46255  fourierdlem66  46412  etransclem37  46511  smfsupmpt  47055  smfinfmpt  47059  smflimsuplem8  47067  eldmressn  47279  afvres  47414  ndmaovrcl  47446  2ltceilhalf  47570  minusmodnep2tmod  47595  modmknepk  47604  mod2addne  47606  modm2nep1  47608  modm1nep2  47610  modm1nem2  47611  modm1p1ne  47612  sprsymrelfv  47736  fmtnofz04prm  47819  31prm  47839  stgr0  48202  stgr1  48203  gpgiedgdmellem  48288  gpgvtx1  48296  gpgedgvtx1  48304  gpgedg2iv  48309  gpg5nbgrvtx13starlem2  48314  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem6  48366  2zrngamnd  48489  2zrngacmnd  48490  2zrngagrp  48491  2zrngALT  48496  2zrngnmlid  48497  2zrngnmlid2  48499  fldhmsubcALTV  48575  lincvalsng  48658  snlindsntor  48713  lincresunit3lem2  48722  lincresunit3  48723  ldepsnlinc  48750  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862  rrx2pnecoorneor  48957  rrx2linest  48984  rrx2linesl  48985  isorcl  49274  catcrcl  49636  setc2othin  49707