Theorem rspccva 3576

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  disjne  4408  n0snor2el  4793  seex  5610  preddowncl  6335  frpoins3g  6349  foelrn  7107  foelrnf  7108  caofid0l  7726  caofid0r  7727  caofid1  7728  caofid2  7729  onnseq  8352  odi  8587  omsmolem  8666  naddssim  8695  fvixp  8930  unblem1  9284  ordiso2  9509  unwdomg  9578  ac5num  10115  acni2  10125  fodomacn  10135  iundom2g  10624  fpwwe2lem3  10718  eltsk2g  10836  tskpwss  10837  tskpw  10838  tsken  10839  prlem934  11118  dedekindle  11474  ltord1  11842  leord1  11843  eqord1  11844  ltord2  11845  leord2  11846  eqord2  11847  supmul1  12286  seqcaopr2  14181  bccl  14466  hashbc  14598  limsupbnd2  15650  2clim  15739  climsup  15837  caurcvg2  15845  caucvgb  15847  isummulc2  15928  telfsumo2  15970  fsumparts  15973  incexclem  16005  isumshft  16008  climcndslem1  16018  climcndslem2  16019  supcvg  16025  geomulcvg  16045  mertenslem2  16054  mertens  16055  bpolycl  16218  bpolydif  16221  rpnnen2lem10  16391  dvdsprime  16862  fuciso  18153  lubub  18685  lubl  18686  mgmlrid  18847  grpinvalem  18854  grpinvex  19154  issubg2  19352  issubg4  19356  nmzbi  19374  gagrpid  19508  cntzi  19543  psgnunilem2  19709  sylow1lem3  19814  pgpfi  19819  slwispgp  19825  sylow2alem1  19831  dprdfcl  20229  ablfac2  20305  abveq0  21075  issrngd  21112  phllmhm  21938  ipcl  21939  ipeq0  21944  isphld  21960  ocvi  21975  pf1ind  22673  cayhamlem3  23205  elcls3  23401  neindisj2  23441  perfi  23473  cnima  23583  1stcfb  23763  1stcelcls  23780  llyi  23793  nllyi  23794  locfinnei  23842  1stckgenlem  23872  ptbasin  23896  txcls  23923  ptcnp  23941  ufli  24233  tgpt0  24438  tsmsxplem2  24473  nrmmetd  24893  tngngp  24973  tngngp3  24975  reperflem  25138  lebnumlem3  25284  htpyi  25295  htpycc  25301  phtpyi  25305  cfili  25589  cmetcvg  25606  caubl  25629  caublcls  25630  bcthlem2  25646  bcthlem3  25647  bcthlem4  25648  ovolicc2lem1  25838  ovolicc2lem5  25842  ovolicc2  25843  voliunlem3  25873  volsuplem  25876  uniioombllem2  25904  mbfima  25951  ismbfd  25960  ismbf3d  25975  mbfmullem  26046  itg2monolem1  26071  itg2i1fseqle  26075  itg2i1fseq  26076  itg2i1fseq2  26077  itg2addlem  26079  bddmulibl  26159  bddiblnc  26162  c1liplem1  26316  dvfsumle  26341  dvfsumabs  26343  dvfsumrlimf  26345  dvfsumlem1  26346  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsumrlimge0  26350  dvfsum2  26354  ftc1lem6  26361  ulmcau  26722  ulmdvlem1  26727  ulmdvlem3  26729  mtestbdd  26732  itgulm  26735  radcnvlem1  26740  abelthlem5  26762  abelthlem7  26765  areambl  27286  2lgslem1a  27718  dchrisumlem2  27817  dchrvmasumiflem1  27828  pntpbnd1  27913  ostthlem1  27954  madebday  28286  addscom  28352  precsexlem9  28601  peano5n0s  28705  bdayfinbndlem1  28853  tglowdim1i  28964  brbtwn2  29483  ax5seglem1  29506  ax5seglem2  29507  ax5seglem9  29515  axcontlem4  29545  axcontlem12  29553  fusgreghash2wsp  30939  grpoidinvlem3  31108  grpoidinv  31110  grpoidinv2  31117  vcidOLD  31166  minvecolem5  31483  hcaucvg  31788  hlimconvi  31793  lnopeq0i  32609  cnlnadjlem5  32673  csmdsymi  32936  difunielsiga  34765  eulerpartlemb  35000  ballotlemfc0  35125  ballotlemfcc  35126  werankwe  35739  elscottrankss  35747  ptpconn  35998  cvmsdisj  36035  cvmshmeo  36036  snmlflim  36097  elmrsubrn  36285  mvtinf  36320  sinccvg  36438  nmulprop  36939  fnemeet1  37154  fnemeet2  37155  fnejoin1  37156  fnejoin2  37157  bj-seex  37834  poimirlem27  38565  poimirlem32  38570  mblfinlem1  38575  ovoliunnfl  38580  ex-ovoliunnfl  38581  voliunnfl  38582  volsupnfl  38583  mbfresfi  38584  itg2gt0cn  38593  ftc1cnnc  38610  ftc1anc  38619  upixp  38663  filbcmb  38674  sdclem1  38677  seqpo  38681  incsequz2  38683  mettrifi  38691  caushft  38695  sstotbnd2  38708  heibor1lem  38743  heiborlem3  38747  heiborlem10  38754  heibor  38755  rrndstprj2  38765  cmpidelt  38793  rngoid  38836  fsuppind  43618  limsuc2  44047  cvgdvgrat  45296  cncmpmax  46048  mccllem  46608  mccl  46609  climinf  46617  climsuse  46619  islptre  46630  limcperiod  46639  addlimc  46657  0ellimcdiv  46658  cncficcgt0  46897  dvbdfbdioolem2  46938  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnprodlem3  46957  stoweidlem7  47016  stoweidlem15  47024  stoweidlem21  47030  stoweidlem31  47040  stoweidlem35  47044  stoweidlem36  47045  stoweidlem50  47059  stoweidlem57  47066  stoweidlem59  47068  wallispilem3  47076  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem32  47148  fourierdlem33  47149  fourierdlem39  47155  fourierdlem62  47177  fourierdlem71  47186  fourierdlem89  47204  fourierdlem91  47206  fourierdlem93  47208  fourierdlem101  47216  fourierdlem103  47218  fourierdlem104  47219  etransclem24  47267  etransclem32  47275  smflimlem6  47785  smfpimcc  47817  smfsuplem2  47821  gricushgr  49014