Theorem rspccva 3580

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is referenced by:  disjne  4415  n0snor2el  4798  seex  5620  preddowncl  6333  frpoins3g  6347  foelrn  7102  foelrnf  7103  caofid0l  7707  caofid0r  7708  caofid1  7709  caofid2  7710  onnseq  8327  odi  8560  omsmolem  8639  naddssim  8668  fvixp  8896  unblem1  9248  ordiso2  9473  unwdomg  9542  ac5num  10016  acni2  10026  fodomacn  10036  iundom2g  10519  fpwwe2lem3  10613  eltsk2g  10731  tskpwss  10732  tskpw  10733  tsken  10734  prlem934  11013  dedekindle  11369  ltord1  11735  leord1  11736  eqord1  11737  ltord2  11738  leord2  11739  eqord2  11740  supmul1  12179  seqcaopr2  14070  bccl  14354  hashbc  14486  limsupbnd2  15530  2clim  15619  climsup  15717  caurcvg2  15725  caucvgb  15727  isummulc2  15809  telfsumo2  15851  fsumparts  15854  incexclem  15886  isumshft  15889  climcndslem1  15899  climcndslem2  15900  supcvg  15906  geomulcvg  15926  mertenslem2  15935  mertens  15936  bpolycl  16101  bpolydif  16104  rpnnen2lem10  16274  dvdsprime  16740  fuciso  18030  lubub  18562  lubl  18563  mgmlrid  18720  grpinvalem  18726  grpinvex  19005  issubg2  19203  issubg4  19207  nmzbi  19225  gagrpid  19359  cntzi  19394  psgnunilem2  19560  sylow1lem3  19665  pgpfi  19670  slwispgp  19676  sylow2alem1  19682  dprdfcl  20080  ablfac2  20156  abveq0  20921  issrngd  20958  phllmhm  21782  ipcl  21783  ipeq0  21788  isphld  21804  ocvi  21819  pf1ind  22515  cayhamlem3  23044  elcls3  23240  neindisj2  23280  perfi  23312  cnima  23422  1stcfb  23602  1stcelcls  23618  llyi  23631  nllyi  23632  locfinnei  23680  1stckgenlem  23710  ptbasin  23734  txcls  23761  ptcnp  23779  ufli  24071  tgpt0  24276  tsmsxplem2  24311  nrmmetd  24731  tngngp  24811  tngngp3  24813  reperflem  24976  lebnumlem3  25122  htpyi  25133  htpycc  25139  phtpyi  25143  cfili  25427  cmetcvg  25444  caubl  25467  caublcls  25468  bcthlem2  25484  bcthlem3  25485  bcthlem4  25486  ovolicc2lem1  25676  ovolicc2lem5  25680  ovolicc2  25681  voliunlem3  25711  volsuplem  25714  uniioombllem2  25742  mbfima  25789  ismbfd  25798  ismbf3d  25813  mbfmullem  25884  itg2monolem1  25909  itg2i1fseqle  25913  itg2i1fseq  25914  itg2i1fseq2  25915  itg2addlem  25917  bddmulibl  25998  bddiblnc  26001  c1liplem1  26155  dvfsumle  26180  dvfsumabs  26182  dvfsumrlimf  26184  dvfsumlem1  26185  dvfsumlem2  26186  dvfsumlem3  26187  dvfsumlem4  26188  dvfsumrlimge0  26189  dvfsum2  26193  ftc1lem6  26200  ulmcau  26558  ulmdvlem1  26563  ulmdvlem3  26565  mtestbdd  26568  itgulm  26571  radcnvlem1  26576  abelthlem5  26598  abelthlem7  26601  areambl  27123  2lgslem1a  27555  dchrisumlem2  27654  dchrvmasumiflem1  27665  pntpbnd1  27750  ostthlem1  27791  madebday  28093  addscom  28159  precsexlem9  28408  peano5n0s  28512  bdayfinbndlem1  28660  tglowdim1i  28770  brbtwn2  29255  ax5seglem1  29278  ax5seglem2  29279  ax5seglem9  29287  axcontlem4  29317  axcontlem12  29325  fusgreghash2wsp  30689  grpoidinvlem3  30858  grpoidinv  30860  grpoidinv2  30867  vcidOLD  30916  minvecolem5  31233  hcaucvg  31538  hlimconvi  31543  lnopeq0i  32359  cnlnadjlem5  32423  csmdsymi  32686  difelsiga  34523  eulerpartlemb  34758  ballotlemfc0  34883  ballotlemfcc  34884  elscottrankss  35516  ptpconn  35725  cvmsdisj  35762  cvmshmeo  35763  snmlflim  35824  elmrsubrn  36012  mvtinf  36047  sinccvg  36165  nmulprop  36682  fnemeet1  36877  fnemeet2  36878  fnejoin1  36879  fnejoin2  36880  bj-seex  37557  poimirlem27  38298  poimirlem32  38303  mblfinlem1  38308  ovoliunnfl  38313  ex-ovoliunnfl  38314  voliunnfl  38315  volsupnfl  38316  mbfresfi  38317  itg2gt0cn  38326  ftc1cnnc  38343  ftc1anc  38352  upixp  38380  filbcmb  38391  sdclem1  38394  seqpo  38398  incsequz2  38400  mettrifi  38408  caushft  38412  sstotbnd2  38425  heibor1lem  38460  heiborlem3  38464  heiborlem10  38471  heibor  38472  rrndstprj2  38482  cmpidelt  38510  rngoid  38553  fsuppind  43322  limsuc2  43768  cvgdvgrat  45023  cncmpmax  45752  mccllem  46313  mccl  46314  climinf  46322  climsuse  46324  islptre  46335  limcperiod  46344  addlimc  46362  0ellimcdiv  46363  cncficcgt0  46602  dvbdfbdioolem2  46643  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnprodlem3  46662  stoweidlem7  46721  stoweidlem15  46729  stoweidlem21  46735  stoweidlem31  46745  stoweidlem35  46749  stoweidlem36  46750  stoweidlem50  46764  stoweidlem57  46771  stoweidlem59  46773  wallispilem3  46781  dirkercncflem2  46818  dirkercncflem4  46820  fourierdlem32  46853  fourierdlem33  46854  fourierdlem39  46860  fourierdlem62  46882  fourierdlem71  46891  fourierdlem89  46909  fourierdlem91  46911  fourierdlem93  46913  fourierdlem101  46921  fourierdlem103  46923  fourierdlem104  46924  etransclem24  46972  etransclem32  46980  smflimlem6  47490  smfpimcc  47522  smfsuplem2  47526  gricushgr  48682