Theorem rspcva 3620

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062

This theorem is referenced by:  rexraleqim  3647  fvn0ssdmfun  7094  fveqdmss  7098  fvcofneq  7113  wfr3g  8347  boxriin  8980  boxcutc  8981  pwssfi  9217  marypha1lem  9473  supmo  9492  infmo  9535  unwdomg  9624  frr3g  9796  isinffi  10032  axdc3lem2  10491  grothac  10870  nqereu  10969  nnsub  12310  zextle  12691  xrsupsslem  13349  xrinfmsslem  13350  supxrunb1  13361  supxrunb2  13362  injresinjlem  13826  ssnn0fi  14026  suppssfz  14035  faclbnd4lem4  14335  ishashinf  14502  rexuz3  15387  cau3lem  15393  caubnd2  15396  o1co  15622  climcn1  15628  incexclem  15872  dvdsext  16358  mreintcl  17638  initoeu1  18056  initoeu2  18061  termoeu1  18063  lublecllem  18405  mgmidmo  18673  gsumval2  18699  dfgrp3lem  19056  symgfix2  19434  odeq  19568  gexid  19599  ringurd  20182  o2timesd  20207  rglcom4d  20208  gsummoncoe1  22312  m2detleiblem3  22635  m2detleiblem4  22636  cpmatmcllem  22724  mp2pm2mplem4  22815  cayleyhamilton1  22898  cmpsublem  23407  cmpsub  23408  cmpfii  23417  ptpjcn  23619  isufil2  23916  ufileu  23927  lmmbr  25292  caussi  25331  plyco0  26231  dgrco  26315  emcllem7  27045  isppw2  27158  addsrid  27997  mulsrid  28139  n0subs  28360  uvtxnbgrvtx  29410  rusgrnumwwlks  29994  clwwlkf  30066  vdgn1frgrv2  30315  frgrregorufr  30344  grpoidinvlem3  30525  grpoideu  30528  lnconi  32052  fsumiunle  32831  tpr2rico  33911  esumiun  34095  0elsiga  34115  sigaclci  34133  dya2icoseg2  34280  derangsn  35175  sat1el2xp  35384  fwddifnp1  36166  poimirlem25  37652  poimirlem26  37653  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  heicant  37662  mblfinlem2  37665  ftc1anc  37708  fdc  37752  bndss  37793  isdrngo2  37965  divrngidl  38035  maxidlmax  38050  cdleme0nex  40292  dihglblem2N  41296  hgmapvs  41893  ismrcd1  42709  nacsfg  42716  isnacs3  42721  nacsfix  42723  mzpcl1  42740  mzpcl2  42741  mzpcong  42984  dnnumch1  43056  aomclem1  43066  aomclem6  43071  lnr2i  43128  hbtlem5  43140  hbt  43142  rexanuz3  45101  choicefi  45205  fsneq  45211  suplesup  45350  xralrple2  45365  infxr  45378  infleinf  45383  xralrple4  45384  xralrple3  45385  xrralrecnnge  45401  supxrunb3  45410  supxrleubrnmpt  45417  unb2ltle  45426  suprleubrnmpt  45433  infxrgelbrnmpt  45465  supminfxr  45475  xrpnf  45496  islpcn  45654  limclner  45666  climd  45687  clim2d  45688  limsupmnflem  45735  limsupre3uzlem  45750  liminflelimsuplem  45790  xlimpnfxnegmnf  45829  xlimxrre  45846  xlimmnfvlem1  45847  xlimmnfv  45849  xlimpnfvlem1  45851  xlimpnfv  45853  climxlim2lem  45860  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  fourierdlem103  46224  fourierdlem104  46225  etransclem48  46297  saluncl  46332  subsaliuncllem  46372  sge0pnffigt  46411  omessle  46513  caragensplit  46515  omeunile  46520  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvle  46615  vonvolmbllem  46675  vonvolmbl  46676  pimdecfgtioc  46730  smfpreimalt  46746  smfpreimaltf  46751  smfpreimale  46769  smfpreimagt  46777  smfpreimage  46797  smfmullem4  46809  smfinflem  46832  iccpartrn  47417  iccpartiun  47421  icceuelpart  47423  lidldomn1  48147  ply1mulgsumlem2  48304  lindslinindsimp2lem5  48379  lindslinindsimp2  48380  snlindsntor  48388  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdig  48544