Theorem rspccva 3582

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082

This theorem is used by:  disjne  4415  n0snor2el  4800  seex  5622  preddowncl  6337  frpoins3g  6351  foelrn  7106  foelrnf  7107  caofid0l  7717  caofid0r  7718  caofid1  7719  caofid2  7720  onnseq  8337  odi  8570  omsmolem  8649  naddssim  8678  fvixp  8906  unblem1  9259  ordiso2  9484  unwdomg  9553  ac5num  10036  acni2  10046  fodomacn  10056  iundom2g  10539  fpwwe2lem3  10633  eltsk2g  10751  tskpwss  10752  tskpw  10753  tsken  10754  prlem934  11033  dedekindle  11389  ltord1  11755  leord1  11756  eqord1  11757  ltord2  11758  leord2  11759  eqord2  11760  supmul1  12199  seqcaopr2  14092  bccl  14376  hashbc  14508  limsupbnd2  15558  2clim  15647  climsup  15745  caurcvg2  15753  caucvgb  15755  isummulc2  15836  telfsumo2  15878  fsumparts  15881  incexclem  15913  isumshft  15916  climcndslem1  15926  climcndslem2  15927  supcvg  15933  geomulcvg  15953  mertenslem2  15962  mertens  15963  bpolycl  16128  bpolydif  16131  rpnnen2lem10  16301  dvdsprime  16767  fuciso  18057  lubub  18589  lubl  18590  mgmlrid  18750  grpinvalem  18757  grpinvex  19054  issubg2  19252  issubg4  19256  nmzbi  19274  gagrpid  19408  cntzi  19443  psgnunilem2  19609  sylow1lem3  19714  pgpfi  19719  slwispgp  19725  sylow2alem1  19731  dprdfcl  20129  ablfac2  20205  abveq0  20971  issrngd  21008  phllmhm  21832  ipcl  21833  ipeq0  21838  isphld  21854  ocvi  21869  pf1ind  22565  cayhamlem3  23094  elcls3  23290  neindisj2  23330  perfi  23362  cnima  23472  1stcfb  23652  1stcelcls  23669  llyi  23682  nllyi  23683  locfinnei  23731  1stckgenlem  23761  ptbasin  23785  txcls  23812  ptcnp  23830  ufli  24122  tgpt0  24327  tsmsxplem2  24362  nrmmetd  24782  tngngp  24862  tngngp3  24864  reperflem  25027  lebnumlem3  25173  htpyi  25184  htpycc  25190  phtpyi  25194  cfili  25478  cmetcvg  25495  caubl  25518  caublcls  25519  bcthlem2  25535  bcthlem3  25536  bcthlem4  25537  ovolicc2lem1  25727  ovolicc2lem5  25731  ovolicc2  25732  voliunlem3  25762  volsuplem  25765  uniioombllem2  25793  mbfima  25840  ismbfd  25849  ismbf3d  25864  mbfmullem  25935  itg2monolem1  25960  itg2i1fseqle  25964  itg2i1fseq  25965  itg2i1fseq2  25966  itg2addlem  25968  bddmulibl  26049  bddiblnc  26052  c1liplem1  26206  dvfsumle  26231  dvfsumabs  26233  dvfsumrlimf  26235  dvfsumlem1  26236  dvfsumlem2  26237  dvfsumlem3  26238  dvfsumlem4  26239  dvfsumrlimge0  26240  dvfsum2  26244  ftc1lem6  26251  ulmcau  26609  ulmdvlem1  26614  ulmdvlem3  26616  mtestbdd  26619  itgulm  26622  radcnvlem1  26627  abelthlem5  26649  abelthlem7  26652  areambl  27174  2lgslem1a  27606  dchrisumlem2  27705  dchrvmasumiflem1  27716  pntpbnd1  27801  ostthlem1  27842  madebday  28144  addscom  28210  precsexlem9  28459  peano5n0s  28563  bdayfinbndlem1  28711  tglowdim1i  28821  brbtwn2  29310  ax5seglem1  29333  ax5seglem2  29334  ax5seglem9  29342  axcontlem4  29372  axcontlem12  29380  fusgreghash2wsp  30760  grpoidinvlem3  30929  grpoidinv  30931  grpoidinv2  30938  vcidOLD  30987  minvecolem5  31304  hcaucvg  31609  hlimconvi  31614  lnopeq0i  32430  cnlnadjlem5  32494  csmdsymi  32757  difunielsiga  34587  eulerpartlemb  34823  ballotlemfc0  34948  ballotlemfcc  34949  elscottrankss  35574  ptpconn  35762  cvmsdisj  35799  cvmshmeo  35800  snmlflim  35861  elmrsubrn  36049  mvtinf  36084  sinccvg  36202  nmulprop  36719  fnemeet1  36934  fnemeet2  36935  fnejoin1  36936  fnejoin2  36937  bj-seex  37614  poimirlem27  38355  poimirlem32  38360  mblfinlem1  38365  ovoliunnfl  38370  ex-ovoliunnfl  38371  voliunnfl  38372  volsupnfl  38373  mbfresfi  38374  itg2gt0cn  38383  ftc1cnnc  38400  ftc1anc  38409  upixp  38438  filbcmb  38449  sdclem1  38452  seqpo  38456  incsequz2  38458  mettrifi  38466  caushft  38470  sstotbnd2  38483  heibor1lem  38518  heiborlem3  38522  heiborlem10  38529  heibor  38530  rrndstprj2  38540  cmpidelt  38568  rngoid  38611  fsuppind  43380  limsuc2  43826  cvgdvgrat  45081  cncmpmax  45810  mccllem  46371  mccl  46372  climinf  46380  climsuse  46382  islptre  46393  limcperiod  46402  addlimc  46420  0ellimcdiv  46421  cncficcgt0  46660  dvbdfbdioolem2  46701  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  dvnprodlem3  46720  stoweidlem7  46779  stoweidlem15  46787  stoweidlem21  46793  stoweidlem31  46803  stoweidlem35  46807  stoweidlem36  46808  stoweidlem50  46822  stoweidlem57  46829  stoweidlem59  46831  wallispilem3  46839  dirkercncflem2  46876  dirkercncflem4  46878  fourierdlem32  46911  fourierdlem33  46912  fourierdlem39  46918  fourierdlem62  46940  fourierdlem71  46949  fourierdlem89  46967  fourierdlem91  46969  fourierdlem93  46971  fourierdlem101  46979  fourierdlem103  46981  fourierdlem104  46982  etransclem24  47030  etransclem32  47038  smflimlem6  47548  smfpimcc  47580  smfsuplem2  47584  gricushgr  48740