Theorem rspccva 3600

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052

This theorem is referenced by:  disjne  4430  n0snor2el  4809  seex  5613  preddowncl  6321  frpoins3g  6335  foelrn  7096  foelrnf  7097  caofid0l  7702  caofid0r  7703  caofid1  7704  caofid2  7705  onnseq  8356  odi  8589  omsmolem  8667  naddssim  8695  fvixp  8914  unblem1  9298  ordiso2  9527  unwdomg  9596  ac5num  10048  acni2  10058  fodomacn  10068  iundom2g  10552  fpwwe2lem3  10645  eltsk2g  10763  tskpwss  10764  tskpw  10765  tsken  10766  prlem934  11045  dedekindle  11397  ltord1  11761  leord1  11762  eqord1  11763  ltord2  11764  leord2  11765  eqord2  11766  supmul1  12209  seqcaopr2  14054  bccl  14338  hashbc  14469  limsupbnd2  15497  2clim  15586  climsup  15684  caurcvg2  15692  caucvgb  15694  isummulc2  15776  telfsumo2  15817  fsumparts  15820  incexclem  15850  isumshft  15853  climcndslem1  15863  climcndslem2  15864  supcvg  15870  geomulcvg  15890  mertenslem2  15899  mertens  15900  bpolycl  16066  bpolydif  16069  rpnnen2lem10  16239  dvdsprime  16704  fuciso  17989  lubub  18519  lubl  18520  mgmlrid  18643  grpinvalem  18649  grpinvex  18924  issubg2  19122  issubg4  19126  nmzbi  19145  gagrpid  19275  cntzi  19310  psgnunilem2  19474  sylow1lem3  19579  pgpfi  19584  slwispgp  19590  sylow2alem1  19596  dprdfcl  19994  ablfac2  20070  abveq0  20776  issrngd  20813  phllmhm  21590  ipcl  21591  ipeq0  21596  isphld  21612  ocvi  21627  pf1ind  22291  cayhamlem3  22823  elcls3  23019  neindisj2  23059  perfi  23091  cnima  23201  1stcfb  23381  1stcelcls  23397  llyi  23410  nllyi  23411  locfinnei  23459  1stckgenlem  23489  ptbasin  23513  txcls  23540  ptcnp  23558  ufli  23850  tgpt0  24055  tsmsxplem2  24090  nrmmetd  24511  tngngp  24591  tngngp3  24593  reperflem  24756  lebnumlem3  24911  htpyi  24922  htpycc  24928  phtpyi  24932  cfili  25218  cmetcvg  25235  caubl  25258  caublcls  25259  bcthlem2  25275  bcthlem3  25276  bcthlem4  25277  ovolicc2lem1  25468  ovolicc2lem5  25472  ovolicc2  25473  voliunlem3  25503  volsuplem  25506  uniioombllem2  25534  mbfima  25581  ismbfd  25590  ismbf3d  25605  mbfmullem  25676  itg2monolem1  25701  itg2i1fseqle  25705  itg2i1fseq  25706  itg2i1fseq2  25707  itg2addlem  25709  bddmulibl  25790  bddiblnc  25793  c1liplem1  25951  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumrlimf  25981  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlimge0  25987  dvfsum2  25991  ftc1lem6  25998  ulmcau  26354  ulmdvlem1  26359  ulmdvlem3  26361  mtestbdd  26364  itgulm  26367  radcnvlem1  26372  abelthlem5  26395  abelthlem7  26398  areambl  26918  2lgslem1a  27352  dchrisumlem2  27451  dchrvmasumiflem1  27462  pntpbnd1  27547  ostthlem1  27588  madebday  27855  addscom  27916  precsexlem9  28156  peano5n0s  28241  zs12bday  28341  tglowdim1i  28426  brbtwn2  28830  ax5seglem1  28853  ax5seglem2  28854  ax5seglem9  28862  axcontlem4  28892  axcontlem12  28900  fusgreghash2wsp  30265  grpoidinvlem3  30433  grpoidinv  30435  grpoidinv2  30442  vcidOLD  30491  minvecolem5  30808  hcaucvg  31113  hlimconvi  31118  lnopeq0i  31934  cnlnadjlem5  31998  csmdsymi  32261  difelsiga  34110  eulerpartlemb  34346  ballotlemfc0  34471  ballotlemfcc  34472  ptpconn  35201  cvmsdisj  35238  cvmshmeo  35239  snmlflim  35300  elmrsubrn  35488  mvtinf  35523  sinccvg  35641  fnemeet1  36330  fnemeet2  36331  fnejoin1  36332  fnejoin2  36333  bj-seex  36886  poimirlem27  37617  poimirlem32  37622  mblfinlem1  37627  ovoliunnfl  37632  ex-ovoliunnfl  37633  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  itg2gt0cn  37645  ftc1cnnc  37662  ftc1anc  37671  upixp  37699  filbcmb  37710  sdclem1  37713  seqpo  37717  incsequz2  37719  mettrifi  37727  caushft  37731  sstotbnd2  37744  heibor1lem  37779  heiborlem3  37783  heiborlem10  37790  heibor  37791  rrndstprj2  37801  cmpidelt  37829  rngoid  37872  fsuppind  42560  limsuc2  43012  cvgdvgrat  44285  cncmpmax  45004  mccllem  45574  mccl  45575  climinf  45583  climsuse  45585  islptre  45596  limcperiod  45605  addlimc  45625  0ellimcdiv  45626  cncficcgt0  45865  dvbdfbdioolem2  45906  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem3  45925  stoweidlem7  45984  stoweidlem15  45992  stoweidlem21  45998  stoweidlem31  46008  stoweidlem35  46012  stoweidlem36  46013  stoweidlem50  46027  stoweidlem57  46034  stoweidlem59  46036  wallispilem3  46044  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem32  46116  fourierdlem33  46117  fourierdlem39  46123  fourierdlem62  46145  fourierdlem71  46154  fourierdlem89  46172  fourierdlem91  46174  fourierdlem93  46176  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  etransclem24  46235  etransclem32  46243  smflimlem6  46753  smfpimcc  46785  smfsuplem2  46789  gricushgr  47878