Theorem eleq2s 2852

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  elrabi  3677  elrabiOLD  3678  optocl  5769  ssrel  5781  eldmeldmressn  6024  predel  6319  fveqdmss  7078  oprabv  7466  elmpocl  7645  el2mpocsbcl  8068  bropopvvv  8073  bropfvvvv  8075  ressuppss  8165  mpoxeldm  8193  mpoxopn0yelv  8195  mpoxopxnop0  8197  tfr2a  8392  rdgseg  8419  2oconcl  8500  ecexr  8705  ectocld  8775  ecoptocl  8798  brecop2  8802  eroveu  8803  mapfvd  8870  mapsnconst  8883  mapfienlem1  9397  mapfienlem2  9398  mapfienlem3  9399  cantnflem2  9682  r1sucg  9761  r1suc  9762  acnrcl  10034  dfac5lem4  10118  fin23lem29  10333  fin23lem30  10334  axcclem  10449  alephval2  10564  0tsk  10747  0nsr  11071  peano2nn  12221  uzssz  12840  peano2uzs  12883  uzsupss  12921  fzssnn  13542  prednn0  13622  fzossnn0  13660  fldiv4p1lem1div2  13797  ltweuz  13923  fzennn  13930  ser1const  14021  expp1  14031  facnn  14232  facp1  14235  bcpasc  14278  hashfzo0  14387  ccatval2  14525  ccatass  14535  swrd00  14591  swrd0  14605  pfx00  14621  pfx0  14622  wrdeqs1cat  14667  splfv2a  14703  revccat  14713  rexuz3  15292  rexanuz2  15293  r19.2uz  15295  rexuzre  15296  cau4  15300  caubnd2  15301  climrlim2  15488  climshft2  15523  climaddc1  15576  climmulc2  15578  climsubc1  15579  climsubc2  15580  climlec2  15602  isercoll2  15612  climsup  15613  climcau  15614  caurcvg  15620  caurcvg2  15621  caucvg  15622  caucvgb  15623  iseraltlem1  15625  iseralt  15628  binomlem  15772  isumshft  15782  cvgrat  15826  clim2div  15832  ntrivcvg  15840  ntrivcvgtail  15843  fprodntriv  15883  fprodeq0  15916  fprodefsum  16035  pwp1fsum  16331  3prm  16628  phicl2  16698  phibndlem  16700  dfphi2  16704  crth  16708  vdwap0  16906  prmlem1a  17037  fvprif  17504  xpsfeq  17506  oppccofval  17658  homarcl2  17982  arwrcl  17991  pleval2i  18286  letsr  18543  gsumws1  18716  smndex1mndlem  18787  mulgnngsum  18954  mulgpropd  18991  psgnunilem2  19358  psgnprfval  19384  gexid  19444  efgmnvl  19577  efgrcl  19578  efgsval  19594  efgs1  19598  efgs1b  19599  frgpuptinv  19634  frgpup3lem  19640  lt6abl  19758  eldprd  19869  isunit  20180  isirred  20226  abvrcl  20422  islss  20538  lbsss  20681  lbssp  20683  lbsind  20684  cssi  21229  thlle  21243  thlleOLD  21244  islbs4  21379  mpfrcl  21640  psr1basf  21717  coe1tm  21787  ply1frcl  21829  mavmulsolcl  22045  marepvcl  22063  1marepvmarrepid  22069  mdet0pr  22086  m2detleiblem1  22118  cramerimplem1  22177  cramerlem1  22181  chpscmat  22336  chpscmatgsumbin  22338  chpscmatgsummon  22339  ptpjpre1  23067  fin1aufil  23428  lmflf  23501  tsmsfbas  23624  xpsxmetlem  23877  xpsmet  23880  metustsym  24056  iscmet3lem3  24799  iscmet3lem1  24800  iscmet3lem2  24801  iscmet3  24802  rrxmvallem  24913  volsup  25065  opnmblALT  25112  itg1val  25192  tdeglem2  25571  ulmcaulem  25898  ulmcau  25899  ulmss  25901  pserdvlem2  25932  eff1olem  26049  logdmnrp  26141  dvlog2lem  26152  logtayl  26160  cxpcn3lem  26245  atancl  26376  atanval  26379  chp1  26661  ppiublem2  26696  lgsdir2lem2  26819  lgsdir2lem3  26820  lgsquadlem2  26874  2lgslem1b  26885  rplogsumlem1  26977  rplogsumlem2  26978  pntlemj  27096  1vgrex  28252  edglnl  28393  usgredg2v  28474  umgrres1lem  28557  upgrres1  28560  nbupgrres  28611  clwlkwlk  29022  wwlksnextproplem1  29153  wwlksnextproplem2  29154  wwlksnextproplem3  29155  rusgrnumwwlkb0  29215  clwlkclwwlklem2a4  29240  eleclclwwlknlem1  29303  eleclclwwlknlem2  29304  erclwwlkneqlen  29311  erclwwlknref  29312  erclwwlknsym  29313  erclwwlkntr  29314  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  frgrnbnb  29536  frgrwopreglem4  29558  frgrwopreglem5  29564  frgrwopreg  29566  numclwlk1  29614  vciOLD  29802  axhcompl-zf  30239  mayete3i  30969  pj3lem1  31447  fzto1stfv1  32248  fzto1st  32250  fzto1stinvn  32251  psgnfzto1st  32252  rmfsupp2  32376  submat1n  32774  xrge0mulc1cn  32910  fiunelros  33161  elmbfmvol2  33255  fibp1  33389  rrvsum  33442  ballotlemfmpn  33482  reprsuc  33616  bnj529  33741  bnj923  33768  bnj570  33905  bnj594  33912  bnj1173  34002  bnj1256  34015  bnj1259  34016  bnj1296  34021  bnj1498  34061  subfacp1lem1  34159  kur14lem7  34192  sat1el2xp  34359  mvrsval  34485  mvrsfpw  34486  mrsubcv  34490  mrsubccat  34498  msubff  34510  msrid  34525  msubvrs  34540  mppsval  34552  divcnvlin  34691  iprodefisumlem  34699  iprodefisum  34700  faclimlem1  34702  onsucsuccmpi  35317  bj-opelresdm  36015  bj-inftyexpitaudisj  36075  bj-inftyexpidisj  36080  bj-ccinftydisj  36083  bj-elccinfty  36084  finixpnum  36462  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem9  36486  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem13  36490  poimirlem14  36491  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem18  36495  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem22  36499  poimirlem29  36506  poimirlem30  36507  broucube  36511  volsupnfl  36522  dvasin  36561  dvacos  36562  sdclem2  36599  fdc  36602  heiborlem4  36671  heiborlem6  36673  smgrpismgmOLD  36719  mndoissmgrpOLD  36725  mndoisexid  36726  rngoueqz  36797  drngoi  36808  mhphflem  41166  prjspertr  41344  prjsperref  41345  prjspersym  41346  prjspreln0  41348  prjspvs  41349  prjsprellsp  41350  jm2.23  41721  wepwsolem  41770  omabs2  42068  omcl3g  42070  trclfvdecomr  42465  mnuprdlem1  43017  mnuprdlem2  43018  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  ssfiunibd  44006  climinf  44309  stoweidlem15  44718  fourierdlem66  44875  etransclem37  44974  smfsupmpt  45518  smflimsuplem8  45530  eldmressn  45734  afvres  45867  ndmaovrcl  45899  sprsymrelfv  46149  fmtnofz04prm  46232  31prm  46252  2zrngamnd  46793  2zrngacmnd  46794  2zrngagrp  46795  2zrngALT  46800  2zrngnmlid  46801  2zrngnmlid2  46803  fldhmsubc  46936  fldhmsubcALTV  46954  lincvalsng  47051  snlindsntor  47106  lincresunit3lem2  47115  lincresunit3  47116  ldepsnlinc  47143  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  rrx2pnecoorneor  47355  rrx2linest  47382  rrx2linesl  47383  setc2othin  47630