Theorem rspcva 3599

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052

This theorem is referenced by:  rexraleqim  3626  fvn0ssdmfun  7063  fveqdmss  7067  fvcofneq  7082  wfr3g  8319  boxriin  8952  boxcutc  8953  pwssfi  9189  marypha1lem  9443  supmo  9462  infmo  9507  unwdomg  9596  frr3g  9768  isinffi  10004  axdc3lem2  10463  grothac  10842  nqereu  10941  nnsub  12282  zextle  12664  xrsupsslem  13321  xrinfmsslem  13322  supxrunb1  13333  supxrunb2  13334  injresinjlem  13801  ssnn0fi  14001  suppssfz  14010  faclbnd4lem4  14312  ishashinf  14479  rexuz3  15365  cau3lem  15371  caubnd2  15374  o1co  15600  climcn1  15606  incexclem  15850  dvdsext  16338  mreintcl  17605  initoeu1  18022  initoeu2  18027  termoeu1  18029  lublecllem  18368  mgmidmo  18636  gsumval2  18662  dfgrp3lem  19019  symgfix2  19395  odeq  19529  gexid  19560  ringurd  20143  o2timesd  20168  rglcom4d  20169  gsummoncoe1  22244  m2detleiblem3  22565  m2detleiblem4  22566  cpmatmcllem  22654  mp2pm2mplem4  22745  cayleyhamilton1  22828  cmpsublem  23335  cmpsub  23336  cmpfii  23345  ptpjcn  23547  isufil2  23844  ufileu  23855  lmmbr  25208  caussi  25247  plyco0  26147  dgrco  26231  emcllem7  26962  isppw2  27075  addsrid  27914  mulsrid  28056  n0subs  28277  uvtxnbgrvtx  29318  rusgrnumwwlks  29902  clwwlkf  29974  vdgn1frgrv2  30223  frgrregorufr  30252  grpoidinvlem3  30433  grpoideu  30436  lnconi  31960  fsumiunle  32754  tpr2rico  33889  esumiun  34071  0elsiga  34091  sigaclci  34109  dya2icoseg2  34256  derangsn  35138  sat1el2xp  35347  fwddifnp1  36129  poimirlem25  37615  poimirlem26  37616  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  heicant  37625  mblfinlem2  37628  ftc1anc  37671  fdc  37715  bndss  37756  isdrngo2  37928  divrngidl  37998  maxidlmax  38013  cdleme0nex  40255  dihglblem2N  41259  hgmapvs  41856  ismrcd1  42668  nacsfg  42675  isnacs3  42680  nacsfix  42682  mzpcl1  42699  mzpcl2  42700  mzpcong  42943  dnnumch1  43015  aomclem1  43025  aomclem6  43030  lnr2i  43087  hbtlem5  43099  hbt  43101  rexanuz3  45068  choicefi  45172  fsneq  45178  suplesup  45314  xralrple2  45329  infxr  45342  infleinf  45347  xralrple4  45348  xralrple3  45349  xrralrecnnge  45365  supxrunb3  45374  supxrleubrnmpt  45381  unb2ltle  45390  suprleubrnmpt  45397  infxrgelbrnmpt  45429  supminfxr  45439  xrpnf  45460  islpcn  45616  limclner  45628  climd  45649  clim2d  45650  limsupmnflem  45697  limsupre3uzlem  45712  xlimpnfxnegmnf  45791  xlimxrre  45808  xlimmnfvlem1  45809  xlimmnfv  45811  xlimpnfvlem1  45813  xlimpnfv  45815  climxlim2lem  45822  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  fourierdlem103  46186  fourierdlem104  46187  etransclem48  46259  saluncl  46294  subsaliuncllem  46334  sge0pnffigt  46373  omessle  46475  caragensplit  46477  omeunile  46482  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvle  46577  vonvolmbllem  46637  vonvolmbl  46638  pimdecfgtioc  46692  smfpreimalt  46708  smfpreimaltf  46713  smfpreimale  46731  smfpreimagt  46739  smfpreimage  46759  smfmullem4  46771  smfinflem  46794  iccpartrn  47392  iccpartiun  47396  icceuelpart  47398  lidldomn1  48154  ply1mulgsumlem2  48311  lindslinindsimp2lem5  48386  lindslinindsimp2  48387  snlindsntor  48395  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdig  48551