Theorem rspcva 3562

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rexraleqim  3589  fvn0ssdmfun  7026  fveqdmss  7030  fvcofneq  7045  wfr3g  8269  boxriin  8888  boxcutc  8889  pwssfi  9111  marypha1lem  9346  supmo  9365  infmo  9410  unwdomg  9499  frr3g  9680  isinffi  9916  axdc3lem2  10373  grothac  10753  nqereu  10852  nnsub  12221  zextle  12602  xrsupsslem  13259  xrinfmsslem  13260  supxrunb1  13271  supxrunb2  13272  injresinjlem  13745  ssnn0fi  13947  suppssfz  13956  faclbnd4lem4  14258  ishashinf  14425  rexuz3  15311  cau3lem  15317  caubnd2  15320  o1co  15548  climcn1  15554  incexclem  15801  dvdsext  16290  mreintcl  17557  initoeu1  17978  initoeu2  17983  termoeu1  17985  lublecllem  18324  mgmidmo  18628  gsumval2  18654  dfgrp3lem  19014  symgfix2  19391  odeq  19525  gexid  19556  ringurd  20166  o2timesd  20191  rglcom4d  20192  gsummoncoe1  22273  m2detleiblem3  22594  m2detleiblem4  22595  cpmatmcllem  22683  mp2pm2mplem4  22774  cayleyhamilton1  22857  cmpsublem  23364  cmpsub  23365  cmpfii  23374  ptpjcn  23576  isufil2  23873  ufileu  23884  lmmbr  25225  caussi  25264  plyco0  26157  dgrco  26240  emcllem7  26965  isppw2  27078  addsrid  27956  mulsrid  28105  n0subs  28355  uvtxnbgrvtx  29462  rusgrnumwwlks  30045  clwwlkf  30117  vdgn1frgrv2  30366  frgrregorufr  30395  grpoidinvlem3  30577  grpoideu  30580  lnconi  32104  fsumiunle  32902  tpr2rico  34056  esumiun  34238  0elsiga  34258  sigaclci  34276  dya2icoseg2  34422  derangsn  35352  sat1el2xp  35561  fwddifnp1  36347  poimirlem25  37966  poimirlem26  37967  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  heicant  37976  mblfinlem2  37979  ftc1anc  38022  fdc  38066  bndss  38107  isdrngo2  38279  divrngidl  38349  maxidlmax  38364  cdleme0nex  40736  dihglblem2N  41740  hgmapvs  42337  ismrcd1  43130  nacsfg  43137  isnacs3  43142  nacsfix  43144  mzpcl1  43161  mzpcl2  43162  mzpcong  43400  dnnumch1  43472  aomclem1  43482  aomclem6  43487  lnr2i  43544  hbtlem5  43556  hbt  43558  rexanuz3  45526  choicefi  45629  fsneq  45635  suplesup  45769  xralrple2  45784  infxr  45796  infleinf  45801  xralrple4  45802  xralrple3  45803  xrralrecnnge  45819  supxrunb3  45828  supxrleubrnmpt  45834  unb2ltle  45843  suprleubrnmpt  45850  infxrgelbrnmpt  45882  supminfxr  45892  xrpnf  45913  islpcn  46067  limclner  46079  climd  46100  clim2d  46101  limsupmnflem  46148  limsupre3uzlem  46163  xlimpnfxnegmnf  46242  xlimxrre  46259  xlimmnfvlem1  46260  xlimmnfv  46262  xlimpnfvlem1  46264  xlimpnfv  46266  climxlim2lem  46273  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  fourierdlem103  46637  fourierdlem104  46638  etransclem48  46710  saluncl  46745  subsaliuncllem  46785  sge0pnffigt  46824  omessle  46926  caragensplit  46928  omeunile  46933  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvle  47028  vonvolmbllem  47088  vonvolmbl  47089  pimdecfgtioc  47143  smfpreimalt  47159  smfpreimaltf  47164  smfpreimale  47182  smfpreimagt  47190  smfpreimage  47210  smfmullem4  47222  smfinflem  47245  iccpartrn  47890  iccpartiun  47894  icceuelpart  47896  lidldomn1  48707  ply1mulgsumlem2  48863  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  snlindsntor  48947  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdig  49099