Theorem eleq2s 2878

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  elrabi  3640  optocl  5744  optoclOLD  5745  ssrel  5758  eldmeldmressn  6013  imadifssranOLD  6202  predel  6324  fveqdmss  7078  oprabv  7480  elmpocl  7662  el2mpocsbcl  8096  bropopvvv  8101  bropfvvvv  8103  ressuppss  8203  mpoxeldm  8231  mpoxopn0yelv  8233  mpoxopxnop0  8235  tfr2a  8406  rdgseg  8433  2oconcl  8514  ecexr  8725  ectocld  8806  ecoptocl  8831  brecop2  8835  eroveu  8836  mapfvd  8910  mapsnconst  8923  mapfienlem1  9400  mapfienlem2  9401  mapfienlem3  9402  cantnflem2  9694  r1sucg  9779  r1suc  9780  karden  9962  acnrcl  10124  dfac5lem4  10208  fin23lem29  10422  fin23lem30  10423  axcclem  10538  alephval2  10660  0tsk  10843  0nsr  11167  peano2nn  12350  uzssz  12989  peano2uzs  13032  uzsupss  13070  fzssnn  13705  prednn0  13789  fzossnn0  13828  fldiv4p1lem1div2  13978  modaddid  14053  ltweuz  14107  fzennn  14114  ser1const  14204  expp1  14214  facnn  14422  facp1  14425  bcpasc  14468  hashfzo0  14578  tpfo  14648  ccatval2  14726  ccatass  14737  swrd00  14796  swrd0  14812  pfx00  14828  pfx0  14829  wrdeqs1cat  14873  splfv2a  14909  revccat  14919  rexuz3  15521  rexanuz2  15522  r19.2uz  15524  rexuzre  15525  cau4  15529  caubnd2  15530  climrlim2  15719  climshft2  15754  climaddc1  15807  climmulc2  15809  climsubc1  15810  climsubc2  15811  climlec2  15831  isercoll2  15841  climsup  15842  climcau  15843  caurcvg  15849  caurcvg2  15850  caucvg  15851  caucvgb  15852  iseraltlem1  15854  iseralt  15857  binomlem  16003  isumshft  16013  cvgrat  16057  clim2div  16063  ntrivcvg  16071  ntrivcvgtail  16074  fprodntriv  16114  fprodeq0  16147  fprodefsum  16266  pwp1fsum  16566  3prm  16874  phicl2  16950  phibndlem  16952  dfphi2  16956  crth  16960  vdwap0  17159  prmlem1a  17289  fvprif  17738  xpsfeq  17740  oppccofval  17895  homarcl2  18215  arwrcl  18224  pleval2i  18513  letsr  18772  gsumws1  19039  smndex1mndlem  19113  mulgnngsum  19294  mulgpropd  19331  psgnunilem2  19714  psgnprfval  19740  gexid  19800  efgmnvl  19933  efgrcl  19934  efgsval  19950  efgs1  19954  efgs1b  19955  frgpuptinv  19990  frgpup3lem  19996  lt6abl  20114  eldprd  20225  isunit  20608  isirred  20654  fldhmsubc  21047  abvrcl  21075  islss  21214  lbsss  21357  lbssp  21359  lbsind  21360  cssi  21995  thlle  22008  islbs4  22143  psrbagleadd1  22241  mpfrcl  22399  psr1basf  22524  coe1tm  22597  ply1frcl  22641  mavmulsolcl  22871  marepvcl  22889  1marepvmarrepid  22895  mdet0pr  22912  m2detleiblem1  22944  cramerimplem1  23006  cramerlem1  23010  chpscmat  23165  chpscmatgsumbin  23167  chpscmatgsummon  23168  ptpjpre1  23895  fin1aufil  24256  lmflf  24329  tsmsfbas  24452  xpsxmetlem  24703  xpsmet  24706  metustsym  24879  iscmet3lem3  25616  iscmet3lem1  25617  iscmet3lem2  25618  iscmet3  25619  rrxmvallem  25730  volsup  25882  opnmblALT  25929  itg1val  26009  tdeglem2  26384  ulmcaulem  26726  ulmcau  26727  ulmss  26729  pserdvlem2  26760  eff1olem  26881  logdmnrp  26974  dvlog2lem  26985  logtayl  26993  cxpcn3lem  27080  atancl  27214  atanval  27217  chp1  27499  ppiublem2  27535  lgsdir2lem2  27658  lgsdir2lem3  27659  lgsquadlem2  27713  2lgslem1b  27724  rplogsumlem1  27816  rplogsumlem2  27817  pntlemj  27935  nnne0s  28728  1vgrex  29585  edglnl  29726  usgredg2v  29813  umgrres1lem  29896  upgrres1  29899  nbupgrres  29950  clwlkwlk  30367  wwlksnextproplem1  30503  wwlksnextproplem2  30504  wwlksnextproplem3  30505  rusgrnumwwlkb0  30568  clwlkclwwlklem2a4  30593  eleclclwwlknlem1  30656  eleclclwwlknlem2  30657  erclwwlkneqlen  30664  erclwwlknref  30665  erclwwlknsym  30666  erclwwlkntr  30667  hashecclwwlkn1  30673  umgrhashecclwwlk  30674  frgrnbnb  30899  frgrwopreglem4  30921  frgrwopreglem5  30927  frgrwopreg  30929  numclwlk1  30977  vciOLD  31168  axhcompl-zf  31605  mayete3i  32335  pj3lem1  32813  fzto1stfv1  33708  fzto1st  33710  fzto1stinvn  33711  psgnfzto1st  33712  rmfsupp2  33844  erler  33872  selvply1rhmlemb  34197  vieta  34258  submat1n  34483  xrge0mulc1cn  34619  fiunelros  34853  elmbfmvol2  34945  fibp1  35079  rrvsum  35132  ballotlemfmpn  35173  reprsuc  35290  bnj529  35418  bnj923  35445  bnj570  35581  bnj594  35588  bnj1173  35678  bnj1256  35691  bnj1259  35692  bnj1296  35697  bnj1498  35737  rankfo  35787  fineqvnttrclselem1  35845  subfacp1lem1  36030  kur14lem7  36063  sat1el2xp  36230  mvrsval  36356  mvrsfpw  36357  mrsubcv  36361  mrsubccat  36369  msubff  36381  msrid  36396  msubvrs  36411  mppsval  36423  divcnvlin  36590  iprodefisumlem  36597  iprodefisum  36598  faclimlem1  36600  onsucsuccmpi  37323  bj-opelresdm  38159  bj-inftyexpitaudisj  38219  bj-inftyexpidisj  38224  bj-ccinftydisj  38227  bj-elccinfty  38228  finixpnum  38621  poimirlem5  38636  poimirlem6  38637  poimirlem7  38638  poimirlem8  38639  poimirlem9  38640  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem13  38644  poimirlem14  38645  poimirlem15  38646  poimirlem16  38647  poimirlem17  38648  poimirlem18  38649  poimirlem19  38650  poimirlem20  38651  poimirlem21  38652  poimirlem22  38653  poimirlem29  38660  poimirlem30  38661  broucube  38665  volsupnfl  38676  dvasin  38715  dvacos  38716  sdclem2  38769  fdc  38772  heiborlem4  38841  heiborlem6  38843  smgrpismgmOLD  38889  mndoissmgrpOLD  38895  mndoisexid  38896  rngoueqz  38967  drngoi  38978  dfadjliftmap2  39482  dfblockliftmap2  39486  sucpre  39522  eldisjsim2  39960  redvmptabs  43504  mhphflem  43717  prjspertr  43726  prjsperref  43727  prjspersym  43728  prjspreln0  43730  prjspvs  43731  prjsprellsp  43732  jm2.23  44096  wepwsolem  44142  omabs2  44427  omcl3g  44429  trclfvdecomr  44821  mnuprdlem1  45349  mnuprdlem2  45350  binomcxplemdvbinom  45430  binomcxplemnotnn0  45433  orbitcl  46040  hfstructstruct  46118  hfstructfun  46119  rnhfstructsshf  46120  ssfiunibd  46418  climinf  46711  stoweidlem15  47118  fourierdlem66  47275  etransclem37  47374  smfsupmpt  47918  smfinfmpt  47922  smflimsuplem8  47930  eldmressn  48200  afvres  48335  ndmaovrcl  48367  2ltceilhalf  48495  minusmodnep2tmod  48522  modmknepk  48531  mod2addne  48533  modm2nep1  48535  modm1nep2  48537  modm1nem2  48538  modm1p1ne  48539  sprsymrelfv  48669  fmtnofz04prm  48755  31prm  48775  ppivalnnnprm  48806  indprmfz  48808  stgr0  49151  stgr1  49152  gpgiedgdmellem  49237  gpgvtx1  49245  gpgedgvtx1  49253  gpgedg2iv  49258  gpg5nbgrvtx13starlem2  49263  pgnbgreunbgrlem3  49309  pgnbgreunbgrlem6  49315  2zrngamnd  49437  2zrngacmnd  49438  2zrngagrp  49439  2zrngALT  49444  2zrngnmlid  49445  2zrngnmlid2  49447  fldhmsubcALTV  49523  lincvalsng  49621  snlindsntor  49676  lincresunit3lem2  49685  lincresunit3  49686  ldepsnlinc  49713  nn0sumshdiglemA  49824  nn0sumshdiglemB  49825  rrx2pnecoorneor  49921  rrx2linest  49947  isorcl  50240  catcrcl  50623  setc2othin  50694