Theorem rspcva 3583

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rexraleqim  3610  fvn0ssdmfun  7028  fveqdmss  7032  fvcofneq  7047  wfr3g  8275  boxriin  8890  boxcutc  8891  pwssfi  9118  marypha1lem  9360  supmo  9379  infmo  9424  unwdomg  9513  frr3g  9685  isinffi  9921  axdc3lem2  10380  grothac  10759  nqereu  10858  nnsub  12206  zextle  12583  xrsupsslem  13243  xrinfmsslem  13244  supxrunb1  13255  supxrunb2  13256  injresinjlem  13724  ssnn0fi  13926  suppssfz  13935  faclbnd4lem4  14237  ishashinf  14404  rexuz3  15291  cau3lem  15297  caubnd2  15300  o1co  15528  climcn1  15534  incexclem  15778  dvdsext  16267  mreintcl  17532  initoeu1  17949  initoeu2  17954  termoeu1  17956  lublecllem  18295  mgmidmo  18563  gsumval2  18589  dfgrp3lem  18946  symgfix2  19322  odeq  19456  gexid  19487  ringurd  20070  o2timesd  20095  rglcom4d  20096  gsummoncoe1  22171  m2detleiblem3  22492  m2detleiblem4  22493  cpmatmcllem  22581  mp2pm2mplem4  22672  cayleyhamilton1  22755  cmpsublem  23262  cmpsub  23263  cmpfii  23272  ptpjcn  23474  isufil2  23771  ufileu  23782  lmmbr  25134  caussi  25173  plyco0  26073  dgrco  26157  emcllem7  26888  isppw2  27001  addsrid  27847  mulsrid  27992  n0subs  28229  uvtxnbgrvtx  29296  rusgrnumwwlks  29877  clwwlkf  29949  vdgn1frgrv2  30198  frgrregorufr  30227  grpoidinvlem3  30408  grpoideu  30411  lnconi  31935  fsumiunle  32727  tpr2rico  33875  esumiun  34057  0elsiga  34077  sigaclci  34095  dya2icoseg2  34242  derangsn  35130  sat1el2xp  35339  fwddifnp1  36126  poimirlem25  37612  poimirlem26  37613  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  heicant  37622  mblfinlem2  37625  ftc1anc  37668  fdc  37712  bndss  37753  isdrngo2  37925  divrngidl  37995  maxidlmax  38010  cdleme0nex  40257  dihglblem2N  41261  hgmapvs  41858  ismrcd1  42659  nacsfg  42666  isnacs3  42671  nacsfix  42673  mzpcl1  42690  mzpcl2  42691  mzpcong  42934  dnnumch1  43006  aomclem1  43016  aomclem6  43021  lnr2i  43078  hbtlem5  43090  hbt  43092  rexanuz3  45063  choicefi  45167  fsneq  45173  suplesup  45308  xralrple2  45323  infxr  45336  infleinf  45341  xralrple4  45342  xralrple3  45343  xrralrecnnge  45359  supxrunb3  45368  supxrleubrnmpt  45375  unb2ltle  45384  suprleubrnmpt  45391  infxrgelbrnmpt  45423  supminfxr  45433  xrpnf  45454  islpcn  45610  limclner  45622  climd  45643  clim2d  45644  limsupmnflem  45691  limsupre3uzlem  45706  xlimpnfxnegmnf  45785  xlimxrre  45802  xlimmnfvlem1  45803  xlimmnfv  45805  xlimpnfvlem1  45807  xlimpnfv  45809  climxlim2lem  45816  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  fourierdlem103  46180  fourierdlem104  46181  etransclem48  46253  saluncl  46288  subsaliuncllem  46328  sge0pnffigt  46367  omessle  46469  caragensplit  46471  omeunile  46476  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvle  46571  vonvolmbllem  46631  vonvolmbl  46632  pimdecfgtioc  46686  smfpreimalt  46702  smfpreimaltf  46707  smfpreimale  46725  smfpreimagt  46733  smfpreimage  46753  smfmullem4  46765  smfinflem  46788  iccpartrn  47404  iccpartiun  47408  icceuelpart  47410  lidldomn1  48192  ply1mulgsumlem2  48349  lindslinindsimp2lem5  48424  lindslinindsimp2  48425  snlindsntor  48433  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  nn0sumshdig  48585