Theorem rspccva 3561

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspccva	⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3558	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	impcom 408	1 ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  disjne  4389  n0snor2el  4765  seex  5552  preddowncl  6239  frpoins3g  6253  foelrn  6991  caofid0l  7573  caofid0r  7574  caofid1  7575  caofid2  7576  onnseq  8184  odi  8419  omsmolem  8496  fvixp  8699  unblem1  9075  ordiso2  9283  unwdomg  9352  ac5num  9801  acni2  9811  fodomacn  9821  iundom2g  10305  fpwwe2lem3  10398  eltsk2g  10516  tskpwss  10517  tskpw  10518  tsken  10519  prlem934  10798  dedekindle  11148  ltord1  11510  leord1  11511  eqord1  11512  ltord2  11513  leord2  11514  eqord2  11515  supmul1  11953  seqcaopr2  13768  bccl  14045  hashbc  14174  limsupbnd2  15201  2clim  15290  climsup  15390  caurcvg2  15398  caucvgb  15400  isummulc2  15483  telfsumo2  15524  fsumparts  15527  incexclem  15557  isumshft  15560  climcndslem1  15570  climcndslem2  15571  supcvg  15577  geomulcvg  15597  mertenslem2  15606  mertens  15607  bpolycl  15771  bpolydif  15774  rpnnen2lem10  15941  dvdsprime  16401  fuciso  17702  lubub  18238  lubl  18239  mgmlrid  18360  grprinvlem  18366  grpinvex  18596  issubg2  18779  issubg4  18783  nmzbi  18801  gagrpid  18909  cntzi  18944  psgnunilem2  19112  sylow1lem3  19214  pgpfi  19219  slwispgp  19225  sylow2alem1  19231  dprdfcl  19625  ablfac2  19701  abveq0  20095  issrngd  20130  phllmhm  20846  ipcl  20847  ipeq0  20852  isphld  20868  ocvi  20883  psrbagconf1oOLD  21149  pf1ind  21530  cayhamlem3  22045  elcls3  22243  neindisj2  22283  perfi  22315  cnima  22425  1stcfb  22605  1stcelcls  22621  llyi  22634  nllyi  22635  locfinnei  22683  1stckgenlem  22713  ptbasin  22737  txcls  22764  ptcnp  22782  ufli  23074  tgpt0  23279  tsmsxplem2  23314  nrmmetd  23739  tngngp  23827  tngngp3  23829  reperflem  23990  lebnumlem3  24135  htpyi  24146  htpycc  24152  phtpyi  24156  cfili  24441  cmetcvg  24458  caubl  24481  caublcls  24482  bcthlem2  24498  bcthlem3  24499  bcthlem4  24500  ovolicc2lem1  24690  ovolicc2lem5  24694  ovolicc2  24695  voliunlem3  24725  volsuplem  24728  uniioombllem2  24756  mbfima  24803  ismbfd  24812  ismbf3d  24827  mbfmullem  24899  itg2monolem1  24924  itg2i1fseqle  24928  itg2i1fseq  24929  itg2i1fseq2  24930  itg2addlem  24932  bddmulibl  25012  bddiblnc  25015  c1liplem1  25169  dvfsumle  25194  dvfsumabs  25196  dvfsumrlimf  25198  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsumrlimge0  25203  dvfsum2  25207  ftc1lem6  25214  ulmcau  25563  ulmdvlem1  25568  ulmdvlem3  25570  mtestbdd  25573  itgulm  25576  radcnvlem1  25581  abelthlem5  25603  abelthlem7  25606  areambl  26117  2lgslem1a  26548  dchrisumlem2  26647  dchrvmasumiflem1  26658  pntpbnd1  26743  ostthlem1  26784  tglowdim1i  26871  brbtwn2  27282  ax5seglem1  27305  ax5seglem2  27306  ax5seglem9  27314  axcontlem4  27344  axcontlem12  27352  fusgreghash2wsp  28711  grpoidinvlem3  28877  grpoidinv  28879  grpoidinv2  28886  vcidOLD  28935  minvecolem5  29252  hcaucvg  29557  hlimconvi  29562  lnopeq0i  30378  cnlnadjlem5  30442  csmdsymi  30705  difelsiga  32110  eulerpartlemb  32344  ballotlemfc0  32468  ballotlemfcc  32469  ptpconn  33204  cvmsdisj  33241  cvmshmeo  33242  snmlflim  33303  elmrsubrn  33491  mvtinf  33526  sinccvg  33640  naddssim  33846  madebday  34089  addscom  34138  fnemeet1  34564  fnemeet2  34565  fnejoin1  34566  fnejoin2  34567  bj-seex  35119  poimirlem27  35813  poimirlem32  35818  mblfinlem1  35823  ovoliunnfl  35828  ex-ovoliunnfl  35829  voliunnfl  35830  volsupnfl  35831  mbfresfi  35832  itg2gt0cn  35841  ftc1cnnc  35858  ftc1anc  35867  upixp  35896  filbcmb  35907  sdclem1  35910  seqpo  35914  incsequz2  35916  mettrifi  35924  caushft  35928  sstotbnd2  35941  heibor1lem  35976  heiborlem3  35980  heiborlem10  35987  heibor  35988  rrndstprj2  35998  cmpidelt  36026  rngoid  36069  fsuppind  40286  limsuc2  40873  cvgdvgrat  41938  cncmpmax  42582  foelrnf  42731  mccllem  43145  mccl  43146  climinf  43154  climsuse  43156  islptre  43167  limcperiod  43176  addlimc  43196  0ellimcdiv  43197  cncficcgt0  43436  dvbdfbdioolem2  43477  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem3  43496  stoweidlem7  43555  stoweidlem15  43563  stoweidlem21  43569  stoweidlem31  43579  stoweidlem35  43583  stoweidlem36  43584  stoweidlem50  43598  stoweidlem57  43605  stoweidlem59  43607  wallispilem3  43615  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem32  43687  fourierdlem33  43688  fourierdlem39  43694  fourierdlem62  43716  fourierdlem71  43725  fourierdlem89  43743  fourierdlem91  43745  fourierdlem93  43747  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  etransclem24  43806  etransclem32  43814  smflimlem6  44321  smfpimcc  44352  smfsuplem2  44356  isomushgr  45289