Theorem eleq2s 2719

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  elrabi  3359  epelg  5030  elxpi  5130  optocl  5195  eldmeldmressn  5440  predel  5697  fveqdmss  6354  oprabv  6703  elmpt2cl  6876  el2mpt2csbcl  7250  bropopvvv  7255  bropfvvvv  7257  ressuppss  7314  mpt2xeldm  7337  mpt2xopn0yelv  7339  mpt2xopxnop0  7341  tfr2a  7491  rdgseg  7518  2oconcl  7583  ecexr  7747  ectocld  7814  ecoptocl  7837  brecop2  7841  eroveu  7842  mapsnconst  7903  mapfienlem1  8310  mapfienlem2  8311  mapfienlem3  8312  cantnflem2  8587  r1sucg  8632  r1suc  8633  acnrcl  8865  dfac5lem4  8949  fin23lem29  9163  fin23lem30  9164  axcclem  9279  alephval2  9394  0tsk  9577  0nsr  9900  peano2nn  11032  uzssz  11707  peano2uzs  11742  uzsupss  11780  fzssnn  12385  prednn0  12463  fzossnn0  12499  fldiv4p1lem1div2  12636  ltweuz  12760  fzennn  12767  ser1const  12857  expp1  12867  facnn  13062  facp1  13065  bcpasc  13108  hashfzo0  13217  ccatval2  13362  ccatass  13371  swrd00  13418  swrd0  13434  wrdeqs1cat  13474  splfv2a  13507  revccat  13515  rexuz3  14088  rexanuz2  14089  r19.2uz  14091  rexuzre  14092  cau4  14096  caubnd2  14097  climrlim2  14278  climshft2  14313  climaddc1  14365  climmulc2  14367  climsubc1  14368  climsubc2  14369  climlec2  14389  isercoll2  14399  climsup  14400  climcau  14401  caurcvg  14407  caurcvg2  14408  caucvg  14409  caucvgb  14410  iseraltlem1  14412  iseralt  14415  binomlem  14561  isumshft  14571  cvgrat  14615  clim2div  14621  ntrivcvg  14629  ntrivcvgtail  14632  fprodntriv  14672  fprodeq0  14705  fprodefsum  14825  pwp1fsum  15114  3prm  15406  phicl2  15473  phibndlem  15475  dfphi2  15479  crth  15483  vdwap0  15680  prmlem1a  15813  xpscfv  16222  xpsfeq  16224  oppccofval  16376  homarcl2  16685  arwrcl  16694  pleval2i  16964  letsr  17227  gsumws1  17376  mulgpropd  17584  psgnunilem2  17915  psgnprfval  17941  gexid  17996  efgmnvl  18127  efgrcl  18128  efgsval  18144  efgs1  18148  efgs1b  18149  frgpuptinv  18184  frgpup3lem  18190  lt6abl  18296  eldprd  18403  isunit  18657  isirred  18699  abvrcl  18821  islss  18935  lbsss  19077  lbssp  19079  lbsind  19080  mpfrcl  19518  psr1basf  19571  coe1tm  19643  ply1frcl  19683  cssi  20028  thlle  20041  islbs4  20171  mavmulsolcl  20357  marepvcl  20375  1marepvmarrepid  20381  mdet0pr  20398  m2detleiblem1  20430  cramerimplem1  20489  cramerlem1  20493  chpscmat  20647  chpscmatgsumbin  20649  chpscmatgsummon  20650  ptpjpre1  21374  fin1aufil  21736  lmflf  21809  tsmsfbas  21931  xpsxmetlem  22184  xpsmet  22187  metustsym  22360  iscmet3lem3  23088  iscmet3lem1  23089  iscmet3lem2  23090  iscmet3  23091  rrxmvallem  23187  volsup  23324  opnmblALT  23371  itg1val  23450  tdeglem2  23821  ulmcaulem  24148  ulmcau  24149  ulmss  24151  pserdvlem2  24182  eff1olem  24294  logdmnrp  24387  dvlog2lem  24398  logtayl  24406  cxpcn3lem  24488  atancl  24608  atanval  24611  chp1  24893  ppiublem2  24928  lgsdir2lem2  25051  lgsdir2lem3  25052  lgsquadlem2  25106  2lgslem1b  25117  rplogsumlem1  25173  rplogsumlem2  25174  pntlemj  25292  1vgrex  25882  edglnl  26038  usgredg2v  26119  umgrres1lem  26202  upgrres1  26205  nbupgrres  26266  clwlkwlk  26671  wwlksnextproplem1  26804  wwlksnextproplem2  26805  wwlksnextproplem3  26806  rusgrnumwwlkb0  26866  clwlkclwwlklem2a4  26898  eleclclwwlksnlem1  26938  eleclclwwlksnlem2  26939  erclwwlksneqlen  26945  erclwwlksnref  26946  erclwwlksnsym  26947  erclwwlksntr  26948  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksf1clwwlk  26969  frgrnbnb  27157  frgrwopreglem4  27179  frgrwopreglem5  27185  frgrwopreg  27187  vciOLD  27416  axhcompl-zf  27855  mayete3i  28587  pj3lem1  29065  fzto1stfv1  29851  fzto1st  29853  fzto1stinvn  29854  psgnfzto1st  29855  submat1n  29871  xrge0mulc1cn  29987  fiunelros  30237  elmbfmvol2  30329  fibp1  30463  rrvsum  30516  ballotlemfmpn  30556  reprsuc  30693  bnj529  30811  bnj923  30838  bnj570  30975  bnj594  30982  bnj1173  31070  bnj1256  31083  bnj1259  31084  bnj1296  31089  bnj1498  31129  subfacp1lem1  31161  kur14lem7  31194  mvrsval  31402  mvrsfpw  31403  mrsubcv  31407  mrsubccat  31415  msubff  31427  msrid  31442  msubvrs  31457  mppsval  31469  divcnvlin  31618  iprodefisumlem  31626  iprodefisum  31627  faclimlem1  31629  onsucsuccmpi  32442  bj-inftyexpidisj  33097  bj-ccinftydisj  33100  bj-elccinfty  33101  finixpnum  33394  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem29  33438  poimirlem30  33439  broucube  33443  volsupnfl  33454  dvasin  33496  dvacos  33497  sdclem2  33538  fdc  33541  heiborlem4  33613  heiborlem6  33615  smgrpismgmOLD  33661  mndoissmgrpOLD  33667  mndoisexid  33668  rngoueqz  33739  drngoi  33750  jm2.23  37563  wepwsolem  37612  trclfvdecomr  38020  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  ssfiunibd  39523  climinf  39838  stoweidlem15  40232  fourierdlem66  40389  etransclem37  40488  smflimsuplem8  41033  eldmressn  41203  afvres  41252  ndmaovrcl  41284  pfx00  41384  pfx0  41385  fmtnofz04prm  41489  31prm  41512  sprsymrelfv  41744  2zrngamnd  41941  2zrngacmnd  41942  2zrngagrp  41943  2zrngALT  41948  2zrngnmlid  41949  2zrngnmlid2  41951  fldhmsubc  42084  fldhmsubcALTV  42102  lincvalsng  42205  snlindsntor  42260  lincresunit3lem2  42269  lincresunit3  42270  ldepsnlinc  42297  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414