Theorem rspcva 3586

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 3584	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rexraleqim  3613  fvn0ssdmfun  7046  fveqdmss  7050  fvcofneq  7065  wfr3g  8298  boxriin  8913  boxcutc  8914  pwssfi  9141  marypha1lem  9384  supmo  9403  infmo  9448  unwdomg  9537  frr3g  9709  isinffi  9945  axdc3lem2  10404  grothac  10783  nqereu  10882  nnsub  12230  zextle  12607  xrsupsslem  13267  xrinfmsslem  13268  supxrunb1  13279  supxrunb2  13280  injresinjlem  13748  ssnn0fi  13950  suppssfz  13959  faclbnd4lem4  14261  ishashinf  14428  rexuz3  15315  cau3lem  15321  caubnd2  15324  o1co  15552  climcn1  15558  incexclem  15802  dvdsext  16291  mreintcl  17556  initoeu1  17973  initoeu2  17978  termoeu1  17980  lublecllem  18319  mgmidmo  18587  gsumval2  18613  dfgrp3lem  18970  symgfix2  19346  odeq  19480  gexid  19511  ringurd  20094  o2timesd  20119  rglcom4d  20120  gsummoncoe1  22195  m2detleiblem3  22516  m2detleiblem4  22517  cpmatmcllem  22605  mp2pm2mplem4  22696  cayleyhamilton1  22779  cmpsublem  23286  cmpsub  23287  cmpfii  23296  ptpjcn  23498  isufil2  23795  ufileu  23806  lmmbr  25158  caussi  25197  plyco0  26097  dgrco  26181  emcllem7  26912  isppw2  27025  addsrid  27871  mulsrid  28016  n0subs  28253  uvtxnbgrvtx  29320  rusgrnumwwlks  29904  clwwlkf  29976  vdgn1frgrv2  30225  frgrregorufr  30254  grpoidinvlem3  30435  grpoideu  30438  lnconi  31962  fsumiunle  32754  tpr2rico  33902  esumiun  34084  0elsiga  34104  sigaclci  34122  dya2icoseg2  34269  derangsn  35157  sat1el2xp  35366  fwddifnp1  36153  poimirlem25  37639  poimirlem26  37640  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  heicant  37649  mblfinlem2  37652  ftc1anc  37695  fdc  37739  bndss  37780  isdrngo2  37952  divrngidl  38022  maxidlmax  38037  cdleme0nex  40284  dihglblem2N  41288  hgmapvs  41885  ismrcd1  42686  nacsfg  42693  isnacs3  42698  nacsfix  42700  mzpcl1  42717  mzpcl2  42718  mzpcong  42961  dnnumch1  43033  aomclem1  43043  aomclem6  43048  lnr2i  43105  hbtlem5  43117  hbt  43119  rexanuz3  45090  choicefi  45194  fsneq  45200  suplesup  45335  xralrple2  45350  infxr  45363  infleinf  45368  xralrple4  45369  xralrple3  45370  xrralrecnnge  45386  supxrunb3  45395  supxrleubrnmpt  45402  unb2ltle  45411  suprleubrnmpt  45418  infxrgelbrnmpt  45450  supminfxr  45460  xrpnf  45481  islpcn  45637  limclner  45649  climd  45670  clim2d  45671  limsupmnflem  45718  limsupre3uzlem  45733  xlimpnfxnegmnf  45812  xlimxrre  45829  xlimmnfvlem1  45830  xlimmnfv  45832  xlimpnfvlem1  45834  xlimpnfv  45836  climxlim2lem  45843  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  fourierdlem103  46207  fourierdlem104  46208  etransclem48  46280  saluncl  46315  subsaliuncllem  46355  sge0pnffigt  46394  omessle  46496  caragensplit  46498  omeunile  46503  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvle  46598  vonvolmbllem  46658  vonvolmbl  46659  pimdecfgtioc  46713  smfpreimalt  46729  smfpreimaltf  46734  smfpreimale  46752  smfpreimagt  46760  smfpreimage  46780  smfmullem4  46792  smfinflem  46815  iccpartrn  47431  iccpartiun  47435  icceuelpart  47437  lidldomn1  48219  ply1mulgsumlem2  48376  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  snlindsntor  48460  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdig  48612