Theorem eleq2s 2883

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840

This theorem is referenced by:  elrabi  3649  optocl  5746  optoclOLD  5747  ssrel  5760  eldmeldmressn  6015  predel  6312  fveqdmss  7063  oprabv  7460  elmpocl  7641  el2mpocsbcl  8068  bropopvvv  8073  bropfvvvv  8075  ressuppss  8167  mpoxeldm  8195  mpoxopn0yelv  8197  mpoxopxnop0  8199  tfr2a  8370  rdgseg  8397  2oconcl  8476  ecexr  8687  ectocld  8768  ecoptocl  8793  brecop2  8797  eroveu  8798  mapfvd  8865  mapsnconst  8878  mapfienlem1  9353  mapfienlem2  9354  mapfienlem3  9355  cantnflem2  9647  r1sucg  9729  r1suc  9730  acnrcl  10014  dfac5lem4  10098  fin23lem29  10313  fin23lem30  10314  axcclem  10429  alephval2  10545  0tsk  10728  0nsr  11052  peano2nn  12236  uzssz  12874  peano2uzs  12917  uzsupss  12955  fzssnn  13587  prednn0  13671  fzossnn0  13710  fldiv4p1lem1div2  13859  modaddid  13934  ltweuz  13988  fzennn  13995  ser1const  14085  expp1  14095  facnn  14302  facp1  14305  bcpasc  14348  hashfzo0  14457  tpfo  14527  ccatval2  14605  ccatass  14616  swrd00  14672  swrd0  14686  pfx00  14702  pfx0  14703  wrdeqs1cat  14747  splfv2a  14783  revccat  14793  rexuz3  15390  rexanuz2  15391  r19.2uz  15393  rexuzre  15394  cau4  15398  caubnd2  15399  climrlim2  15588  climshft2  15623  climaddc1  15676  climmulc2  15678  climsubc1  15679  climsubc2  15680  climlec2  15700  isercoll2  15710  climsup  15711  climcau  15712  caurcvg  15718  caurcvg2  15719  caucvg  15720  caucvgb  15721  iseraltlem1  15723  iseralt  15726  binomlem  15873  isumshft  15883  cvgrat  15927  clim2div  15933  ntrivcvg  15941  ntrivcvgtail  15944  fprodntriv  15986  fprodeq0  16019  fprodefsum  16139  pwp1fsum  16439  3prm  16742  phicl2  16817  phibndlem  16819  dfphi2  16823  crth  16827  vdwap0  17026  prmlem1a  17156  fvprif  17605  xpsfeq  17607  oppccofval  17762  homarcl2  18082  arwrcl  18091  pleval2i  18380  letsr  18639  gsumws1  18887  smndex1mndlem  18961  mulgnngsum  19136  mulgpropd  19173  psgnunilem2  19556  psgnprfval  19582  gexid  19642  efgmnvl  19775  efgrcl  19776  efgsval  19792  efgs1  19796  efgs1b  19797  frgpuptinv  19832  frgpup3lem  19838  lt6abl  19956  eldprd  20067  isunit  20446  isirred  20492  fldhmsubc  20857  abvrcl  20885  islss  21024  lbsss  21167  lbssp  21169  lbsind  21170  cssi  21794  thlle  21807  islbs4  21942  psrbagleadd1  22038  mpfrcl  22196  psr1basf  22321  coe1tm  22394  ply1frcl  22439  mavmulsolcl  22669  marepvcl  22687  1marepvmarrepid  22693  mdet0pr  22710  m2detleiblem1  22742  cramerimplem1  22801  cramerlem1  22805  chpscmat  22960  chpscmatgsumbin  22962  chpscmatgsummon  22963  ptpjpre1  23689  fin1aufil  24050  lmflf  24123  tsmsfbas  24246  xpsxmetlem  24497  xpsmet  24500  metustsym  24673  iscmet3lem3  25410  iscmet3lem1  25411  iscmet3lem2  25412  iscmet3  25413  rrxmvallem  25524  volsup  25676  opnmblALT  25723  itg1val  25803  tdeglem2  26179  ulmcaulem  26515  ulmcau  26516  ulmss  26518  pserdvlem2  26549  eff1olem  26671  logdmnrp  26764  dvlog2lem  26775  logtayl  26783  cxpcn3lem  26870  atancl  27004  atanval  27007  chp1  27289  ppiublem2  27325  lgsdir2lem2  27448  lgsdir2lem3  27449  lgsquadlem2  27503  2lgslem1b  27514  rplogsumlem1  27606  rplogsumlem2  27607  pntlemj  27725  nnne0s  28488  1vgrex  29261  edglnl  29402  usgredg2v  29486  umgrres1lem  29569  upgrres1  29572  nbupgrres  29623  clwlkwlk  30033  wwlksnextproplem1  30167  wwlksnextproplem2  30168  wwlksnextproplem3  30169  rusgrnumwwlkb0  30232  clwlkclwwlklem2a4  30257  eleclclwwlknlem1  30320  eleclclwwlknlem2  30321  erclwwlkneqlen  30328  erclwwlknref  30329  erclwwlknsym  30330  erclwwlkntr  30331  hashecclwwlkn1  30337  umgrhashecclwwlk  30338  frgrnbnb  30553  frgrwopreglem4  30575  frgrwopreglem5  30581  frgrwopreg  30583  numclwlk1  30631  vciOLD  30822  axhcompl-zf  31259  mayete3i  31989  pj3lem1  32467  fzto1stfv1  33334  fzto1st  33336  fzto1stinvn  33337  psgnfzto1st  33338  rmfsupp2  33470  erler  33498  selvply1rhmlemb  33826  vieta  33887  submat1n  34112  xrge0mulc1cn  34248  fiunelros  34481  elmbfmvol2  34574  fibp1  34708  rrvsum  34761  ballotlemfmpn  34802  reprsuc  34919  bnj529  35047  bnj923  35074  bnj570  35210  bnj594  35217  bnj1173  35307  bnj1256  35320  bnj1259  35321  bnj1296  35326  bnj1498  35366  fineqvnttrclselem1  35429  subfacp1lem1  35542  kur14lem7  35575  sat1el2xp  35742  mvrsval  35868  mvrsfpw  35869  mrsubcv  35873  mrsubccat  35881  msubff  35893  msrid  35908  msubvrs  35923  mppsval  35935  divcnvlin  36096  iprodefisumlem  36103  iprodefisum  36104  faclimlem1  36106  onsucsuccmpi  36816  bj-opelresdm  37649  bj-inftyexpitaudisj  37709  bj-inftyexpidisj  37714  bj-ccinftydisj  37717  bj-elccinfty  37718  finixpnum  38116  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem14  38145  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem29  38160  poimirlem30  38161  broucube  38165  volsupnfl  38176  dvasin  38215  dvacos  38216  sdclem2  38253  fdc  38256  heiborlem4  38325  heiborlem6  38327  smgrpismgmOLD  38373  mndoissmgrpOLD  38379  mndoisexid  38380  rngoueqz  38451  drngoi  38462  dfadjliftmap2  38968  dfblockliftmap2  38972  sucpre  39008  eldisjsim2  39446  redvmptabs  42981  mhphflem  43190  prjspertr  43199  prjsperref  43200  prjspersym  43201  prjspreln0  43203  prjspvs  43204  prjsprellsp  43205  jm2.23  43585  wepwsolem  43631  omabs2  43921  omcl3g  43923  trclfvdecomr  44316  mnuprdlem1  44846  mnuprdlem2  44847  binomcxplemdvbinom  44927  binomcxplemnotnn0  44930  orbitcl  45531  ssfiunibd  45886  climinf  46180  stoweidlem15  46587  fourierdlem66  46744  etransclem37  46843  smfsupmpt  47387  smfinfmpt  47391  smflimsuplem8  47399  eldmressn  47629  afvres  47764  ndmaovrcl  47796  2ltceilhalf  47924  minusmodnep2tmod  47951  modmknepk  47960  mod2addne  47962  modm2nep1  47964  modm1nep2  47966  modm1nem2  47967  modm1p1ne  47968  sprsymrelfv  48098  fmtnofz04prm  48184  31prm  48204  ppivalnnnprm  48235  indprmfz  48237  stgr0  48580  stgr1  48581  gpgiedgdmellem  48666  gpgvtx1  48674  gpgedgvtx1  48682  gpgedg2iv  48687  gpg5nbgrvtx13starlem2  48692  pgnbgreunbgrlem3  48738  pgnbgreunbgrlem6  48744  2zrngamnd  48867  2zrngacmnd  48868  2zrngagrp  48869  2zrngALT  48874  2zrngnmlid  48875  2zrngnmlid2  48877  fldhmsubcALTV  48953  lincvalsng  49047  snlindsntor  49102  lincresunit3lem2  49111  lincresunit3  49112  ldepsnlinc  49139  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251  rrx2pnecoorneor  49346  rrx2linest  49373  rrx2linesl  49374  isorcl  49662  catcrcl  50024  setc2othin  50095