Theorem rspcva 3579

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcva	⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3577	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 410	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077

This theorem is referenced by:  rexraleqim  3606  fsneq  7016  fvn0ssdmfun  7055  fveqdmss  7059  fvcofneq  7074  wfr3g  8300  boxriin  8922  boxcutc  8923  pwssfi  9145  marypha1lem  9379  supmo  9398  infmo  9443  unwdomg  9532  frr3g  9714  isinffi  9950  axdc3lem2  10408  grothac  10788  nqereu  10887  nnsub  12257  zextle  12646  xrsupsslem  13310  xrinfmsslem  13311  supxrunb1  13322  supxrunb2  13323  injresinjlem  13796  ssnn0fi  13998  suppssfz  14007  faclbnd4lem4  14309  ishashinf  14476  rexuz3  15376  cau3lem  15382  caubnd2  15385  o1co  15613  climcn1  15619  incexclem  15866  dvdsext  16355  mreintcl  17623  initoeu1  18044  initoeu2  18049  termoeu1  18051  lublecllem  18390  mgmidmo  18694  gsumval2  18720  dfgrp3lem  19080  symgfix2  19456  odeq  19590  gexid  19621  ringurd  20235  o2timesd  20260  rglcom4d  20261  gsummoncoe1  22371  m2detleiblem3  22689  m2detleiblem4  22690  cpmatmcllem  22778  mp2pm2mplem4  22869  cayleyhamilton1  22952  cmpsublem  23459  cmpsub  23460  cmpfii  23469  ptpjcn  23671  isufil2  23968  ufileu  23979  lmmbr  25320  caussi  25359  plyco0  26252  dgrco  26335  emcllem7  27066  isppw2  27179  addsrid  28057  mulsrid  28206  n0subs  28456  uvtxnbgrvtx  29594  rusgrnumwwlks  30177  clwwlkf  30249  vdgn1frgrv2  30498  frgrregorufr  30527  grpoidinvlem3  30709  grpoideu  30712  lnconi  32236  fsumiunle  33031  tpr2rico  34209  esumiun  34391  0elsiga  34411  sigaclci  34429  dya2icoseg2  34575  derangsn  35520  sat1el2xp  35729  fwddifnp1  36515  poimirlem25  38144  poimirlem26  38145  poimirlem30  38149  poimirlem31  38150  poimirlem32  38151  heicant  38154  mblfinlem2  38157  ftc1anc  38200  fdc  38244  bndss  38285  isdrngo2  38457  divrngidl  38527  maxidlmax  38542  cdleme0nex  40914  dihglblem2N  41918  hgmapvs  42515  ismrcd1  43279  nacsfg  43286  isnacs3  43291  nacsfix  43293  mzpcl1  43310  mzpcl2  43311  mzpcong  43549  dnnumch1  43621  aomclem1  43631  aomclem6  43636  lnr2i  43693  hbtlem5  43705  hbt  43707  rexanuz3  45674  choicefi  45777  suplesup  45915  xralrple2  45930  infxr  45942  infleinf  45947  xralrple4  45948  xralrple3  45949  xrralrecnnge  45965  supxrunb3  45974  supxrleubrnmpt  45980  unb2ltle  45989  suprleubrnmpt  45996  infxrgelbrnmpt  46028  supminfxr  46038  xrpnf  46059  islpcn  46213  limclner  46225  climd  46246  clim2d  46247  limsupmnflem  46294  limsupre3uzlem  46309  xlimpnfxnegmnf  46388  xlimxrre  46405  xlimmnfvlem1  46406  xlimmnfv  46408  xlimpnfvlem1  46410  xlimpnfv  46412  climxlim2lem  46419  ioodvbdlimc1lem1  46505  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  fourierdlem103  46783  fourierdlem104  46784  etransclem48  46856  saluncl  46891  subsaliuncllem  46931  sge0pnffigt  46970  omessle  47072  caragensplit  47074  omeunile  47079  hoidmvlelem2  47170  hoidmvlelem3  47171  hoidmvle  47174  vonvolmbllem  47234  vonvolmbl  47235  pimdecfgtioc  47289  smfpreimalt  47305  smfpreimaltf  47310  smfpreimale  47328  smfpreimagt  47336  smfpreimage  47356  smfmullem4  47368  smfinflem  47391  iccpartrn  48036  iccpartiun  48040  icceuelpart  48042  lidldomn1  48853  ply1mulgsumlem2  49009  lindslinindsimp2lem5  49084  lindslinindsimp2  49085  snlindsntor  49093  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  nn0sumshdig  49245