Theorem eleq2s 2880

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

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

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 2147  ax-9 2155  ax-ext 2734

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

This theorem is used by:  elrabi  3644  optocl  5753  optoclOLD  5754  ssrel  5767  eldmeldmressn  6022  imadifssran  6201  predel  6323  fveqdmss  7075  oprabv  7477  elmpocl  7659  el2mpocsbcl  8086  bropopvvv  8091  bropfvvvv  8093  ressuppss  8185  mpoxeldm  8213  mpoxopn0yelv  8215  mpoxopxnop0  8217  tfr2a  8388  rdgseg  8415  2oconcl  8494  ecexr  8705  ectocld  8786  ecoptocl  8811  brecop2  8815  eroveu  8816  mapfvd  8890  mapsnconst  8903  mapfienlem1  9379  mapfienlem2  9380  mapfienlem3  9381  cantnflem2  9673  r1sucg  9755  r1suc  9756  karden  9902  acnrcl  10049  dfac5lem4  10133  fin23lem29  10347  fin23lem30  10348  axcclem  10463  alephval2  10585  0tsk  10768  0nsr  11092  peano2nn  12273  uzssz  12912  peano2uzs  12955  uzsupss  12993  fzssnn  13627  prednn0  13711  fzossnn0  13750  fldiv4p1lem1div2  13900  modaddid  13975  ltweuz  14029  fzennn  14036  ser1const  14126  expp1  14136  facnn  14343  facp1  14346  bcpasc  14389  hashfzo0  14499  tpfo  14569  ccatval2  14647  ccatass  14658  swrd00  14716  swrd0  14732  pfx00  14748  pfx0  14749  wrdeqs1cat  14793  splfv2a  14829  revccat  14839  rexuz3  15440  rexanuz2  15441  r19.2uz  15443  rexuzre  15444  cau4  15448  caubnd2  15449  climrlim2  15638  climshft2  15673  climaddc1  15726  climmulc2  15728  climsubc1  15729  climsubc2  15730  climlec2  15750  isercoll2  15760  climsup  15761  climcau  15762  caurcvg  15768  caurcvg2  15769  caucvg  15770  caucvgb  15771  iseraltlem1  15773  iseralt  15776  binomlem  15922  isumshft  15932  cvgrat  15976  clim2div  15982  ntrivcvg  15990  ntrivcvgtail  15993  fprodntriv  16035  fprodeq0  16068  fprodefsum  16187  pwp1fsum  16487  3prm  16790  phicl2  16865  phibndlem  16867  dfphi2  16871  crth  16875  vdwap0  17074  prmlem1a  17204  fvprif  17653  xpsfeq  17655  oppccofval  17810  homarcl2  18130  arwrcl  18139  pleval2i  18428  letsr  18687  gsumws1  18953  smndex1mndlem  19027  mulgnngsum  19208  mulgpropd  19245  psgnunilem2  19628  psgnprfval  19654  gexid  19714  efgmnvl  19847  efgrcl  19848  efgsval  19864  efgs1  19868  efgs1b  19869  frgpuptinv  19904  frgpup3lem  19910  lt6abl  20028  eldprd  20139  isunit  20520  isirred  20566  fldhmsubc  20957  abvrcl  20985  islss  21124  lbsss  21267  lbssp  21269  lbsind  21270  cssi  21903  thlle  21916  islbs4  22051  psrbagleadd1  22149  mpfrcl  22307  psr1basf  22432  coe1tm  22505  ply1frcl  22549  mavmulsolcl  22779  marepvcl  22797  1marepvmarrepid  22803  mdet0pr  22820  m2detleiblem1  22852  cramerimplem1  22914  cramerlem1  22918  chpscmat  23073  chpscmatgsumbin  23075  chpscmatgsummon  23076  ptpjpre1  23803  fin1aufil  24164  lmflf  24237  tsmsfbas  24360  xpsxmetlem  24611  xpsmet  24614  metustsym  24787  iscmet3lem3  25524  iscmet3lem1  25525  iscmet3lem2  25526  iscmet3  25527  rrxmvallem  25638  volsup  25790  opnmblALT  25837  itg1val  25917  tdeglem2  26293  ulmcaulem  26637  ulmcau  26638  ulmss  26640  pserdvlem2  26671  eff1olem  26793  logdmnrp  26886  dvlog2lem  26897  logtayl  26905  cxpcn3lem  26992  atancl  27126  atanval  27129  chp1  27411  ppiublem2  27447  lgsdir2lem2  27570  lgsdir2lem3  27571  lgsquadlem2  27625  2lgslem1b  27636  rplogsumlem1  27728  rplogsumlem2  27729  pntlemj  27847  nnne0s  28610  1vgrex  29467  edglnl  29608  usgredg2v  29695  umgrres1lem  29778  upgrres1  29781  nbupgrres  29832  clwlkwlk  30249  wwlksnextproplem1  30385  wwlksnextproplem2  30386  wwlksnextproplem3  30387  rusgrnumwwlkb0  30450  clwlkclwwlklem2a4  30475  eleclclwwlknlem1  30538  eleclclwwlknlem2  30539  erclwwlkneqlen  30546  erclwwlknref  30547  erclwwlknsym  30548  erclwwlkntr  30549  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  frgrnbnb  30781  frgrwopreglem4  30803  frgrwopreglem5  30809  frgrwopreg  30811  numclwlk1  30859  vciOLD  31050  axhcompl-zf  31487  mayete3i  32217  pj3lem1  32695  fzto1stfv1  33549  fzto1st  33551  fzto1stinvn  33552  psgnfzto1st  33553  rmfsupp2  33685  erler  33713  selvply1rhmlemb  34037  vieta  34098  submat1n  34323  xrge0mulc1cn  34459  fiunelros  34693  elmbfmvol2  34786  fibp1  34920  rrvsum  34973  ballotlemfmpn  35014  reprsuc  35131  bnj529  35259  bnj923  35286  bnj570  35422  bnj594  35429  bnj1173  35519  bnj1256  35532  bnj1259  35533  bnj1296  35538  bnj1498  35578  rankfo  35627  fineqvnttrclselem1  35655  subfacp1lem1  35766  kur14lem7  35799  sat1el2xp  35966  mvrsval  36092  mvrsfpw  36093  mrsubcv  36097  mrsubccat  36105  msubff  36117  msrid  36132  msubvrs  36147  mppsval  36159  divcnvlin  36320  iprodefisumlem  36327  iprodefisum  36328  faclimlem1  36330  onsucsuccmpi  37070  bj-opelresdm  37905  bj-inftyexpitaudisj  37965  bj-inftyexpidisj  37970  bj-ccinftydisj  37973  bj-elccinfty  37974  finixpnum  38367  poimirlem5  38382  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem14  38391  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem29  38406  poimirlem30  38407  broucube  38411  volsupnfl  38422  dvasin  38461  dvacos  38462  sdclem2  38500  fdc  38503  heiborlem4  38572  heiborlem6  38574  smgrpismgmOLD  38620  mndoissmgrpOLD  38626  mndoisexid  38627  rngoueqz  38698  drngoi  38709  dfadjliftmap2  39213  dfblockliftmap2  39217  sucpre  39253  eldisjsim2  39691  redvmptabs  43243  mhphflem  43450  prjspertr  43459  prjsperref  43460  prjspersym  43461  prjspreln0  43463  prjspvs  43464  prjsprellsp  43465  jm2.23  43845  wepwsolem  43891  omabs2  44181  omcl3g  44183  trclfvdecomr  44576  mnuprdlem1  45104  mnuprdlem2  45105  binomcxplemdvbinom  45185  binomcxplemnotnn0  45188  orbitcl  45788  ssfiunibd  46150  climinf  46444  stoweidlem15  46851  fourierdlem66  47008  etransclem37  47107  smfsupmpt  47651  smfinfmpt  47655  smflimsuplem8  47663  eldmressn  47933  afvres  48068  ndmaovrcl  48100  2ltceilhalf  48228  minusmodnep2tmod  48255  modmknepk  48264  mod2addne  48266  modm2nep1  48268  modm1nep2  48270  modm1nem2  48271  modm1p1ne  48272  sprsymrelfv  48402  fmtnofz04prm  48488  31prm  48508  ppivalnnnprm  48539  indprmfz  48541  stgr0  48884  stgr1  48885  gpgiedgdmellem  48970  gpgvtx1  48978  gpgedgvtx1  48986  gpgedg2iv  48991  gpg5nbgrvtx13starlem2  48996  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem6  49048  2zrngamnd  49170  2zrngacmnd  49171  2zrngagrp  49172  2zrngALT  49177  2zrngnmlid  49178  2zrngnmlid2  49180  fldhmsubcALTV  49256  lincvalsng  49354  snlindsntor  49409  lincresunit3lem2  49418  lincresunit3  49419  ldepsnlinc  49446  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  rrx2pnecoorneor  49653  rrx2linest  49680  rrx2linesl  49681  isorcl  49967  catcrcl  50329  setc2othin  50400