Theorem rspcva 3581

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082

This theorem is used by:  rexraleqim  3608  fsneq  7034  fvn0ssdmfun  7073  fveqdmss  7077  fvcofneq  7092  wfr3g  8322  boxriin  8944  boxcutc  8945  pwssfi  9168  marypha1lem  9400  supmo  9419  infmo  9464  unwdomg  9553  frr3g  9735  isinffi  9994  axdc3lem2  10450  grothac  10830  nqereu  10929  nnsub  12295  zextle  12685  xrsupsslem  13349  xrinfmsslem  13350  supxrunb1  13361  supxrunb2  13362  injresinjlem  13836  ssnn0fi  14039  suppssfz  14048  faclbnd4lem4  14350  ishashinf  14518  rexuz3  15424  cau3lem  15430  caubnd2  15433  o1co  15661  climcn1  15667  incexclem  15913  dvdsext  16401  mreintcl  17669  initoeu1  18090  initoeu2  18095  termoeu1  18097  lublecllem  18436  mgmidmo  18742  gsumval2  18776  dfgrp3lem  19148  symgfix2  19530  odeq  19664  gexid  19695  ringurd  20311  o2timesd  20336  rglcom4d  20337  gsummoncoe1  22518  m2detleiblem3  22836  m2detleiblem4  22837  cpmatmcllem  22925  mp2pm2mplem4  23016  cayleyhamilton1  23099  cmpsublem  23606  cmpsub  23607  cmpfii  23616  ptpjcn  23819  isufil2  24116  ufileu  24127  lmmbr  25468  caussi  25507  plyco0  26400  dgrco  26483  emcllem7  27217  isppw2  27330  addsrid  28208  mulsrid  28357  n0subs  28607  uvtxnbgrvtx  29801  rusgrnumwwlks  30393  clwwlkf  30465  vdgn1frgrv2  30718  frgrregorufr  30747  grpoidinvlem3  30929  grpoideu  30932  lnconi  32456  fsumiunle  33243  tpr2rico  34366  esumiun  34548  0elsiga  34568  sigaclci  34586  dya2icoseg2  34733  derangsn  35699  sat1el2xp  35908  fwddifnp1  36694  poimirlem25  38353  poimirlem26  38354  poimirlem30  38358  poimirlem31  38359  poimirlem32  38360  heicant  38363  mblfinlem2  38366  ftc1anc  38409  fdc  38454  bndss  38495  isdrngo2  38667  divrngidl  38737  maxidlmax  38752  cdleme0nex  41122  dihglblem2N  42126  hgmapvs  42723  ismrcd1  43487  nacsfg  43494  isnacs3  43499  nacsfix  43501  mzpcl1  43518  mzpcl2  43519  mzpcong  43757  dnnumch1  43829  aomclem1  43839  aomclem6  43844  lnr2i  43901  hbtlem5  43913  hbt  43915  rexanuz3  45872  choicefi  45975  suplesup  46113  xralrple2  46128  infxr  46140  infleinf  46145  xralrple4  46146  xralrple3  46147  xrralrecnnge  46163  supxrunb3  46172  supxrleubrnmpt  46178  unb2ltle  46187  suprleubrnmpt  46194  infxrgelbrnmpt  46226  supminfxr  46236  xrpnf  46257  islpcn  46411  limclner  46423  climd  46444  clim2d  46445  limsupmnflem  46492  limsupre3uzlem  46507  xlimpnfxnegmnf  46586  xlimxrre  46603  xlimmnfvlem1  46604  xlimmnfv  46606  xlimpnfvlem1  46608  xlimpnfv  46610  climxlim2lem  46617  ioodvbdlimc1lem1  46703  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  fourierdlem103  46981  fourierdlem104  46982  etransclem48  47054  saluncl  47089  subsaliuncllem  47129  sge0pnffigt  47168  omessle  47270  caragensplit  47272  omeunile  47277  hoidmvlelem2  47368  hoidmvlelem3  47369  hoidmvle  47372  vonvolmbllem  47432  vonvolmbl  47433  pimdecfgtioc  47487  smfpreimalt  47503  smfpreimaltf  47508  smfpreimale  47526  smfpreimagt  47534  smfpreimage  47554  smfmullem4  47566  smfinflem  47589  iccpartrn  48237  iccpartiun  48241  icceuelpart  48243  lidldomn1  49053  ply1mulgsumlem2  49224  lindslinindsimp2lem5  49299  lindslinindsimp2  49300  snlindsntor  49308  nn0sumshdiglemA  49456  nn0sumshdiglemB  49457  nn0sumshdig  49460