Theorem eleq2s 2931

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  elrabi  3675  epelgOLD  5467  elxpi  5577  optocl  5645  eldmeldmressn  5896  predel  6165  fveqdmss  6846  oprabv  7214  elmpocl  7387  el2mpocsbcl  7780  bropopvvv  7785  bropfvvvv  7787  ressuppss  7849  mpoxeldm  7877  mpoxopn0yelv  7879  mpoxopxnop0  7881  tfr2a  8031  rdgseg  8058  2oconcl  8128  ecexr  8294  ectocld  8364  ecoptocl  8387  brecop2  8391  eroveu  8392  mapfvd  8443  mapsnconst  8456  mapfienlem1  8868  mapfienlem2  8869  mapfienlem3  8870  cantnflem2  9153  r1sucg  9198  r1suc  9199  acnrcl  9468  dfac5lem4  9552  fin23lem29  9763  fin23lem30  9764  axcclem  9879  alephval2  9994  0tsk  10177  0nsr  10501  peano2nn  11650  uzssz  12265  peano2uzs  12303  uzsupss  12341  fzssnn  12952  prednn0  13032  fzossnn0  13069  fldiv4p1lem1div2  13206  ltweuz  13330  fzennn  13337  ser1const  13427  expp1  13437  facnn  13636  facp1  13639  bcpasc  13682  hashfzo0  13792  ccatval2  13932  ccatass  13942  swrd00  14006  swrd0  14020  pfx00  14036  pfx0  14037  wrdeqs1cat  14082  splfv2a  14118  revccat  14128  rexuz3  14708  rexanuz2  14709  r19.2uz  14711  rexuzre  14712  cau4  14716  caubnd2  14717  climrlim2  14904  climshft2  14939  climaddc1  14991  climmulc2  14993  climsubc1  14994  climsubc2  14995  climlec2  15015  isercoll2  15025  climsup  15026  climcau  15027  caurcvg  15033  caurcvg2  15034  caucvg  15035  caucvgb  15036  iseraltlem1  15038  iseralt  15041  binomlem  15184  isumshft  15194  cvgrat  15239  clim2div  15245  ntrivcvg  15253  ntrivcvgtail  15256  fprodntriv  15296  fprodeq0  15329  fprodefsum  15448  pwp1fsum  15742  3prm  16038  phicl2  16105  phibndlem  16107  dfphi2  16111  crth  16115  vdwap0  16312  prmlem1a  16440  fvprif  16834  xpsfeq  16836  oppccofval  16986  homarcl2  17295  arwrcl  17304  pleval2i  17574  letsr  17837  gsumws1  18002  smndex1mndlem  18074  mulgnngsum  18233  mulgpropd  18269  psgnunilem2  18623  psgnprfval  18649  gexid  18706  efgmnvl  18840  efgrcl  18841  efgsval  18857  efgs1  18861  efgs1b  18862  frgpuptinv  18897  frgpup3lem  18903  lt6abl  19015  eldprd  19126  isunit  19407  isirred  19449  abvrcl  19592  islss  19706  lbsss  19849  lbssp  19851  lbsind  19852  mpfrcl  20298  psr1basf  20369  coe1tm  20441  ply1frcl  20481  cssi  20828  thlle  20841  islbs4  20976  mavmulsolcl  21160  marepvcl  21178  1marepvmarrepid  21184  mdet0pr  21201  m2detleiblem1  21233  cramerimplem1  21292  cramerlem1  21296  chpscmat  21450  chpscmatgsumbin  21452  chpscmatgsummon  21453  ptpjpre1  22179  fin1aufil  22540  lmflf  22613  tsmsfbas  22736  xpsxmetlem  22989  xpsmet  22992  metustsym  23165  iscmet3lem3  23893  iscmet3lem1  23894  iscmet3lem2  23895  iscmet3  23896  rrxmvallem  24007  volsup  24157  opnmblALT  24204  itg1val  24284  tdeglem2  24655  ulmcaulem  24982  ulmcau  24983  ulmss  24985  pserdvlem2  25016  eff1olem  25132  logdmnrp  25224  dvlog2lem  25235  logtayl  25243  cxpcn3lem  25328  atancl  25459  atanval  25462  chp1  25744  ppiublem2  25779  lgsdir2lem2  25902  lgsdir2lem3  25903  lgsquadlem2  25957  2lgslem1b  25968  rplogsumlem1  26060  rplogsumlem2  26061  pntlemj  26179  1vgrex  26787  edglnl  26928  usgredg2v  27009  umgrres1lem  27092  upgrres1  27095  nbupgrres  27146  clwlkwlk  27556  wwlksnextproplem1  27688  wwlksnextproplem2  27689  wwlksnextproplem3  27690  rusgrnumwwlkb0  27750  clwlkclwwlklem2a4  27775  eleclclwwlknlem1  27839  eleclclwwlknlem2  27840  erclwwlkneqlen  27847  erclwwlknref  27848  erclwwlknsym  27849  erclwwlkntr  27850  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  frgrnbnb  28072  frgrwopreglem4  28094  frgrwopreglem5  28100  frgrwopreg  28102  numclwlk1  28150  vciOLD  28338  axhcompl-zf  28775  mayete3i  29505  pj3lem1  29983  fzto1stfv1  30743  fzto1st  30745  fzto1stinvn  30746  psgnfzto1st  30747  rmfsupp2  30866  submat1n  31070  xrge0mulc1cn  31184  fiunelros  31433  elmbfmvol2  31525  fibp1  31659  rrvsum  31712  ballotlemfmpn  31752  reprsuc  31886  bnj529  32012  bnj923  32039  bnj570  32177  bnj594  32184  bnj1173  32274  bnj1256  32287  bnj1259  32288  bnj1296  32293  bnj1498  32333  subfacp1lem1  32426  kur14lem7  32459  sat1el2xp  32626  mvrsval  32752  mvrsfpw  32753  mrsubcv  32757  mrsubccat  32765  msubff  32777  msrid  32792  msubvrs  32807  mppsval  32819  divcnvlin  32964  iprodefisumlem  32972  iprodefisum  32973  faclimlem1  32975  onsucsuccmpi  33791  bj-opelresdm  34440  bj-inftyexpitaudisj  34490  bj-inftyexpidisj  34495  bj-ccinftydisj  34498  bj-elccinfty  34499  finixpnum  34892  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem9  34916  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem29  34936  poimirlem30  34937  broucube  34941  volsupnfl  34952  dvasin  34993  dvacos  34994  sdclem2  35032  fdc  35035  heiborlem4  35107  heiborlem6  35109  smgrpismgmOLD  35155  mndoissmgrpOLD  35161  mndoisexid  35162  rngoueqz  35233  drngoi  35244  prjspertr  39304  prjsperref  39305  prjspersym  39306  prjspreln0  39308  prjspvs  39309  prjsprellsp  39310  jm2.23  39642  wepwsolem  39691  trclfvdecomr  40122  mnuprdlem1  40657  mnuprdlem2  40658  binomcxplemdvbinom  40734  binomcxplemnotnn0  40737  ssfiunibd  41625  climinf  41936  stoweidlem15  42349  fourierdlem66  42506  etransclem37  42605  smflimsuplem8  43150  eldmressn  43321  afvres  43420  ndmaovrcl  43452  sprsymrelfv  43705  fmtnofz04prm  43788  31prm  43809  2zrngamnd  44261  2zrngacmnd  44262  2zrngagrp  44263  2zrngALT  44268  2zrngnmlid  44269  2zrngnmlid2  44271  fldhmsubc  44404  fldhmsubcALTV  44422  lincvalsng  44520  snlindsntor  44575  lincresunit3lem2  44584  lincresunit3  44585  ldepsnlinc  44612  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  rrx2pnecoorneor  44751  rrx2linest  44778  rrx2linesl  44779