Theorem rspccva 3563

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  disjne  4395  n0snor2el  4776  seex  5590  preddowncl  6296  frpoins3g  6310  foelrn  7059  foelrnf  7060  caofid0l  7664  caofid0r  7665  caofid1  7666  caofid2  7667  onnseq  8284  odi  8514  omsmolem  8593  naddssim  8621  fvixp  8850  unblem1  9202  ordiso2  9430  unwdomg  9499  ac5num  9958  acni2  9968  fodomacn  9978  iundom2g  10462  fpwwe2lem3  10556  eltsk2g  10674  tskpwss  10675  tskpw  10676  tsken  10677  prlem934  10956  dedekindle  11310  ltord1  11676  leord1  11677  eqord1  11678  ltord2  11679  leord2  11680  eqord2  11681  supmul1  12125  seqcaopr2  14000  bccl  14284  hashbc  14415  limsupbnd2  15445  2clim  15534  climsup  15632  caurcvg2  15640  caucvgb  15642  isummulc2  15724  telfsumo2  15766  fsumparts  15769  incexclem  15801  isumshft  15804  climcndslem1  15814  climcndslem2  15815  supcvg  15821  geomulcvg  15841  mertenslem2  15850  mertens  15851  bpolycl  16017  bpolydif  16020  rpnnen2lem10  16190  dvdsprime  16656  fuciso  17945  lubub  18477  lubl  18478  mgmlrid  18635  grpinvalem  18641  grpinvex  18919  issubg2  19117  issubg4  19121  nmzbi  19139  gagrpid  19269  cntzi  19304  psgnunilem2  19470  sylow1lem3  19575  pgpfi  19580  slwispgp  19586  sylow2alem1  19592  dprdfcl  19990  ablfac2  20066  abveq0  20795  issrngd  20832  phllmhm  21612  ipcl  21613  ipeq0  21618  isphld  21634  ocvi  21649  pf1ind  22320  cayhamlem3  22852  elcls3  23048  neindisj2  23088  perfi  23120  cnima  23230  1stcfb  23410  1stcelcls  23426  llyi  23439  nllyi  23440  locfinnei  23488  1stckgenlem  23518  ptbasin  23542  txcls  23569  ptcnp  23587  ufli  23879  tgpt0  24084  tsmsxplem2  24119  nrmmetd  24539  tngngp  24619  tngngp3  24621  reperflem  24784  lebnumlem3  24930  htpyi  24941  htpycc  24947  phtpyi  24951  cfili  25235  cmetcvg  25252  caubl  25275  caublcls  25276  bcthlem2  25292  bcthlem3  25293  bcthlem4  25294  ovolicc2lem1  25484  ovolicc2lem5  25488  ovolicc2  25489  voliunlem3  25519  volsuplem  25522  uniioombllem2  25550  mbfima  25597  ismbfd  25606  ismbf3d  25621  mbfmullem  25692  itg2monolem1  25717  itg2i1fseqle  25721  itg2i1fseq  25722  itg2i1fseq2  25723  itg2addlem  25725  bddmulibl  25806  bddiblnc  25809  c1liplem1  25963  dvfsumle  25988  dvfsumabs  25990  dvfsumrlimf  25992  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlimge0  25997  dvfsum2  26001  ftc1lem6  26008  ulmcau  26360  ulmdvlem1  26365  ulmdvlem3  26367  mtestbdd  26370  itgulm  26373  radcnvlem1  26378  abelthlem5  26400  abelthlem7  26403  areambl  26922  2lgslem1a  27354  dchrisumlem2  27453  dchrvmasumiflem1  27464  pntpbnd1  27549  ostthlem1  27590  madebday  27892  addscom  27958  precsexlem9  28207  peano5n0s  28311  bdayfinbndlem1  28459  tglowdim1i  28569  brbtwn2  28974  ax5seglem1  28997  ax5seglem2  28998  ax5seglem9  29006  axcontlem4  29036  axcontlem12  29044  fusgreghash2wsp  30408  grpoidinvlem3  30577  grpoidinv  30579  grpoidinv2  30586  vcidOLD  30635  minvecolem5  30952  hcaucvg  31257  hlimconvi  31262  lnopeq0i  32078  cnlnadjlem5  32142  csmdsymi  32405  difelsiga  34277  eulerpartlemb  34512  ballotlemfc0  34637  ballotlemfcc  34638  ptpconn  35415  cvmsdisj  35452  cvmshmeo  35453  snmlflim  35514  elmrsubrn  35702  mvtinf  35737  sinccvg  35855  fnemeet1  36548  fnemeet2  36549  fnejoin1  36550  fnejoin2  36551  bj-seex  37229  poimirlem27  37968  poimirlem32  37973  mblfinlem1  37978  ovoliunnfl  37983  ex-ovoliunnfl  37984  voliunnfl  37985  volsupnfl  37986  mbfresfi  37987  itg2gt0cn  37996  ftc1cnnc  38013  ftc1anc  38022  upixp  38050  filbcmb  38061  sdclem1  38064  seqpo  38068  incsequz2  38070  mettrifi  38078  caushft  38082  sstotbnd2  38095  heibor1lem  38130  heiborlem3  38134  heiborlem10  38141  heibor  38142  rrndstprj2  38152  cmpidelt  38180  rngoid  38223  fsuppind  43023  limsuc2  43469  cvgdvgrat  44740  cncmpmax  45463  mccllem  46027  mccl  46028  climinf  46036  climsuse  46038  islptre  46049  limcperiod  46058  addlimc  46076  0ellimcdiv  46077  cncficcgt0  46316  dvbdfbdioolem2  46357  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem3  46376  stoweidlem7  46435  stoweidlem15  46443  stoweidlem21  46449  stoweidlem31  46459  stoweidlem35  46463  stoweidlem36  46464  stoweidlem50  46478  stoweidlem57  46485  stoweidlem59  46487  wallispilem3  46495  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem32  46567  fourierdlem33  46568  fourierdlem39  46574  fourierdlem62  46596  fourierdlem71  46605  fourierdlem89  46623  fourierdlem91  46625  fourierdlem93  46627  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  etransclem24  46686  etransclem32  46694  smflimlem6  47204  smfpimcc  47236  smfsuplem2  47240  gricushgr  48393