Theorem rspcva 3576

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rexraleqim  3603  fvn0ssdmfun  7028  fveqdmss  7032  fvcofneq  7047  wfr3g  8271  boxriin  8890  boxcutc  8891  pwssfi  9113  marypha1lem  9348  supmo  9367  infmo  9412  unwdomg  9501  frr3g  9680  isinffi  9916  axdc3lem2  10373  grothac  10753  nqereu  10852  nnsub  12201  zextle  12577  xrsupsslem  13234  xrinfmsslem  13235  supxrunb1  13246  supxrunb2  13247  injresinjlem  13718  ssnn0fi  13920  suppssfz  13929  faclbnd4lem4  14231  ishashinf  14398  rexuz3  15284  cau3lem  15290  caubnd2  15293  o1co  15521  climcn1  15527  incexclem  15771  dvdsext  16260  mreintcl  17526  initoeu1  17947  initoeu2  17952  termoeu1  17954  lublecllem  18293  mgmidmo  18597  gsumval2  18623  dfgrp3lem  18980  symgfix2  19357  odeq  19491  gexid  19522  ringurd  20132  o2timesd  20157  rglcom4d  20158  gsummoncoe1  22264  m2detleiblem3  22585  m2detleiblem4  22586  cpmatmcllem  22674  mp2pm2mplem4  22765  cayleyhamilton1  22848  cmpsublem  23355  cmpsub  23356  cmpfii  23365  ptpjcn  23567  isufil2  23864  ufileu  23875  lmmbr  25226  caussi  25265  plyco0  26165  dgrco  26249  emcllem7  26980  isppw2  27093  addsrid  27972  mulsrid  28121  n0subs  28371  uvtxnbgrvtx  29478  rusgrnumwwlks  30062  clwwlkf  30134  vdgn1frgrv2  30383  frgrregorufr  30412  grpoidinvlem3  30594  grpoideu  30597  lnconi  32121  fsumiunle  32921  tpr2rico  34090  esumiun  34272  0elsiga  34292  sigaclci  34310  dya2icoseg2  34456  derangsn  35386  sat1el2xp  35595  fwddifnp1  36381  poimirlem25  37896  poimirlem26  37897  poimirlem30  37901  poimirlem31  37902  poimirlem32  37903  heicant  37906  mblfinlem2  37909  ftc1anc  37952  fdc  37996  bndss  38037  isdrngo2  38209  divrngidl  38279  maxidlmax  38294  cdleme0nex  40666  dihglblem2N  41670  hgmapvs  42267  ismrcd1  43055  nacsfg  43062  isnacs3  43067  nacsfix  43069  mzpcl1  43086  mzpcl2  43087  mzpcong  43329  dnnumch1  43401  aomclem1  43411  aomclem6  43416  lnr2i  43473  hbtlem5  43485  hbt  43487  rexanuz3  45455  choicefi  45558  fsneq  45564  suplesup  45698  xralrple2  45713  infxr  45725  infleinf  45730  xralrple4  45731  xralrple3  45732  xrralrecnnge  45748  supxrunb3  45757  supxrleubrnmpt  45764  unb2ltle  45773  suprleubrnmpt  45780  infxrgelbrnmpt  45812  supminfxr  45822  xrpnf  45843  islpcn  45997  limclner  46009  climd  46030  clim2d  46031  limsupmnflem  46078  limsupre3uzlem  46093  xlimpnfxnegmnf  46172  xlimxrre  46189  xlimmnfvlem1  46190  xlimmnfv  46192  xlimpnfvlem1  46194  xlimpnfv  46196  climxlim2lem  46203  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  fourierdlem103  46567  fourierdlem104  46568  etransclem48  46640  saluncl  46675  subsaliuncllem  46715  sge0pnffigt  46754  omessle  46856  caragensplit  46858  omeunile  46863  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvle  46958  vonvolmbllem  47018  vonvolmbl  47019  pimdecfgtioc  47073  smfpreimalt  47089  smfpreimaltf  47094  smfpreimale  47112  smfpreimagt  47120  smfpreimage  47140  smfmullem4  47152  smfinflem  47175  iccpartrn  47790  iccpartiun  47794  icceuelpart  47796  lidldomn1  48591  ply1mulgsumlem2  48747  lindslinindsimp2lem5  48822  lindslinindsimp2  48823  snlindsntor  48831  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  nn0sumshdig  48983