Theorem rspcva 3572

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050

This theorem is referenced by:  rexraleqim  3599  fvn0ssdmfun  7017  fveqdmss  7021  fvcofneq  7036  wfr3g  8259  boxriin  8876  boxcutc  8877  pwssfi  9099  marypha1lem  9334  supmo  9353  infmo  9398  unwdomg  9487  frr3g  9666  isinffi  9902  axdc3lem2  10359  grothac  10739  nqereu  10838  nnsub  12187  zextle  12563  xrsupsslem  13220  xrinfmsslem  13221  supxrunb1  13232  supxrunb2  13233  injresinjlem  13704  ssnn0fi  13906  suppssfz  13915  faclbnd4lem4  14217  ishashinf  14384  rexuz3  15270  cau3lem  15276  caubnd2  15279  o1co  15507  climcn1  15513  incexclem  15757  dvdsext  16246  mreintcl  17512  initoeu1  17933  initoeu2  17938  termoeu1  17940  lublecllem  18279  mgmidmo  18583  gsumval2  18609  dfgrp3lem  18966  symgfix2  19343  odeq  19477  gexid  19508  ringurd  20118  o2timesd  20143  rglcom4d  20144  gsummoncoe1  22250  m2detleiblem3  22571  m2detleiblem4  22572  cpmatmcllem  22660  mp2pm2mplem4  22751  cayleyhamilton1  22834  cmpsublem  23341  cmpsub  23342  cmpfii  23351  ptpjcn  23553  isufil2  23850  ufileu  23861  lmmbr  25212  caussi  25251  plyco0  26151  dgrco  26235  emcllem7  26966  isppw2  27079  addsrid  27934  mulsrid  28082  n0subs  28322  uvtxnbgrvtx  29415  rusgrnumwwlks  29999  clwwlkf  30071  vdgn1frgrv2  30320  frgrregorufr  30349  grpoidinvlem3  30530  grpoideu  30533  lnconi  32057  fsumiunle  32859  tpr2rico  34018  esumiun  34200  0elsiga  34220  sigaclci  34238  dya2icoseg2  34384  derangsn  35313  sat1el2xp  35522  fwddifnp1  36308  poimirlem25  37785  poimirlem26  37786  poimirlem30  37790  poimirlem31  37791  poimirlem32  37792  heicant  37795  mblfinlem2  37798  ftc1anc  37841  fdc  37885  bndss  37926  isdrngo2  38098  divrngidl  38168  maxidlmax  38183  cdleme0nex  40489  dihglblem2N  41493  hgmapvs  42090  ismrcd1  42882  nacsfg  42889  isnacs3  42894  nacsfix  42896  mzpcl1  42913  mzpcl2  42914  mzpcong  43156  dnnumch1  43228  aomclem1  43238  aomclem6  43243  lnr2i  43300  hbtlem5  43312  hbt  43314  rexanuz3  45282  choicefi  45386  fsneq  45392  suplesup  45526  xralrple2  45541  infxr  45553  infleinf  45558  xralrple4  45559  xralrple3  45560  xrralrecnnge  45576  supxrunb3  45585  supxrleubrnmpt  45592  unb2ltle  45601  suprleubrnmpt  45608  infxrgelbrnmpt  45640  supminfxr  45650  xrpnf  45671  islpcn  45825  limclner  45837  climd  45858  clim2d  45859  limsupmnflem  45906  limsupre3uzlem  45921  xlimpnfxnegmnf  46000  xlimxrre  46017  xlimmnfvlem1  46018  xlimmnfv  46020  xlimpnfvlem1  46022  xlimpnfv  46024  climxlim2lem  46031  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  fourierdlem103  46395  fourierdlem104  46396  etransclem48  46468  saluncl  46503  subsaliuncllem  46543  sge0pnffigt  46582  omessle  46684  caragensplit  46686  omeunile  46691  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvle  46786  vonvolmbllem  46846  vonvolmbl  46847  pimdecfgtioc  46901  smfpreimalt  46917  smfpreimaltf  46922  smfpreimale  46940  smfpreimagt  46948  smfpreimage  46968  smfmullem4  46980  smfinflem  47003  iccpartrn  47618  iccpartiun  47622  icceuelpart  47624  lidldomn1  48419  ply1mulgsumlem2  48575  lindslinindsimp2lem5  48650  lindslinindsimp2  48651  snlindsntor  48659  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  nn0sumshdig  48811