Theorem rspccva 3579

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  disjne  4411  n0snor2el  4793  seex  5617  preddowncl  6361  frpoins3g  6375  foelrn  7139  foelrnf  7140  caofid0l  7758  caofid0r  7759  caofid1  7760  caofid2  7761  onnseq  8390  odi  8625  omsmolem  8704  naddssim  8733  fvixp  8968  unblem1  9322  ordiso2  9546  unwdomg  9615  ac5num  10154  acni2  10164  fodomacn  10174  iundom2g  10663  fpwwe2lem3  10757  eltsk2g  10875  tskpwss  10876  tskpw  10877  tsken  10878  prlem934  11157  dedekindle  11513  ltord1  11882  leord1  11883  eqord1  11884  ltord2  11885  leord2  11886  eqord2  11887  supmul1  12326  seqcaopr2  14221  bccl  14507  hashbc  14639  limsupbnd2  15694  2clim  15783  climsup  15881  caurcvg2  15889  caucvgb  15891  isummulc2  15972  telfsumo2  16014  fsumparts  16017  incexclem  16049  isumshft  16052  climcndslem1  16062  climcndslem2  16063  supcvg  16069  geomulcvg  16089  mertenslem2  16098  mertens  16099  bpolycl  16262  bpolydif  16265  rpnnen2lem10  16435  dvdsprime  16906  fuciso  18203  lubub  18735  lubl  18736  mgmlrid  18897  grpinvalem  18904  grpinvex  19204  issubg2  19402  issubg4  19406  nmzbi  19424  gagrpid  19559  cntzi  19594  psgnunilem2  19760  sylow1lem3  19865  pgpfi  19870  slwispgp  19876  sylow2alem1  19882  dprdfcl  20280  ablfac2  20356  abveq0  21126  issrngd  21163  phllmhm  21993  ipcl  21994  ipeq0  21999  isphld  22015  ocvi  22030  pf1ind  22728  cayhamlem3  23260  elcls3  23456  neindisj2  23496  perfi  23528  cnima  23638  1stcfb  23818  1stcelcls  23835  llyi  23848  nllyi  23849  locfinnei  23897  1stckgenlem  23927  ptbasin  23951  txcls  23978  ptcnp  23996  ufli  24288  tgpt0  24493  tsmsxplem2  24528  nrmmetd  24948  tngngp  25028  tngngp3  25030  reperflem  25193  lebnumlem3  25339  htpyi  25350  htpycc  25356  phtpyi  25360  cfili  25644  cmetcvg  25661  caubl  25684  caublcls  25685  bcthlem2  25701  bcthlem3  25702  bcthlem4  25703  ovolicc2lem1  25893  ovolicc2lem5  25897  ovolicc2  25898  voliunlem3  25928  volsuplem  25931  uniioombllem2  25959  mbfima  26006  ismbfd  26015  ismbf3d  26030  mbfmullem  26101  itg2monolem1  26126  itg2i1fseqle  26130  itg2i1fseq  26131  itg2i1fseq2  26132  itg2addlem  26134  bddmulibl  26214  bddiblnc  26217  c1liplem1  26371  dvfsumle  26396  dvfsumabs  26398  dvfsumrlimf  26400  dvfsumlem1  26401  dvfsumlem2  26402  dvfsumlem3  26403  dvfsumlem4  26404  dvfsumrlimge0  26405  dvfsum2  26409  ftc1lem6  26416  ulmcau  26779  ulmdvlem1  26784  ulmdvlem3  26786  mtestbdd  26789  itgulm  26792  radcnvlem1  26797  abelthlem5  26819  abelthlem7  26822  areambl  27343  2lgslem1a  27775  dchrisumlem2  27874  dchrvmasumiflem1  27885  pntpbnd1  27970  ostthlem1  28011  madebday  28343  addscom  28409  precsexlem9  28658  peano5n0s  28762  bdayfinbndlem1  28910  tglowdim1i  29021  brbtwn2  29540  ax5seglem1  29563  ax5seglem2  29564  ax5seglem9  29572  axcontlem4  29602  axcontlem12  29610  fusgreghash2wsp  30996  grpoidinvlem3  31165  grpoidinv  31167  grpoidinv2  31174  vcidOLD  31223  minvecolem5  31540  hcaucvg  31845  hlimconvi  31850  lnopeq0i  32666  cnlnadjlem5  32730  csmdsymi  32993  difunielsiga  34876  eulerpartlemb  35111  ballotlemfc0  35236  ballotlemfcc  35237  werankwe  35862  werankwe2  35863  elscottrankss  35872  ptpconn  36206  cvmsdisj  36243  cvmshmeo  36244  snmlflim  36305  elmrsubrn  36493  mvtinf  36528  sinccvg  36646  nmulprop  37154  fnemeet1  37369  fnemeet2  37370  fnejoin1  37371  fnejoin2  37372  bj-seex  38049  poimirlem27  38833  poimirlem32  38838  mblfinlem1  38843  ovoliunnfl  38848  ex-ovoliunnfl  38849  voliunnfl  38850  volsupnfl  38851  mbfresfi  38852  itg2gt0cn  38861  ftc1cnnc  38878  ftc1anc  38887  upixp  38931  filbcmb  38940  sdclem1  38943  seqpo  38947  incsequz2  38949  mettrifi  38957  caushft  38961  sstotbnd2  38974  heibor1lem  39009  heiborlem3  39013  heiborlem10  39020  heibor  39021  rrndstprj2  39031  cmpidelt  39059  rngoid  39102  fsuppind  43884  limsuc2  44314  cvgdvgrat  45558  cncmpmax  46323  mccllem  46882  mccl  46883  climinf  46891  climsuse  46893  islptre  46904  limcperiod  46913  addlimc  46931  0ellimcdiv  46932  cncficcgt0  47171  dvbdfbdioolem2  47212  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnprodlem3  47231  stoweidlem7  47290  stoweidlem15  47298  stoweidlem21  47304  stoweidlem31  47314  stoweidlem35  47318  stoweidlem36  47319  stoweidlem50  47333  stoweidlem57  47340  stoweidlem59  47342  wallispilem3  47350  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem32  47422  fourierdlem33  47423  fourierdlem39  47429  fourierdlem62  47451  fourierdlem71  47460  fourierdlem89  47478  fourierdlem91  47480  fourierdlem93  47482  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  etransclem24  47541  etransclem32  47549  smflimlem6  48059  smfpimcc  48091  smfsuplem2  48095  gricushgr  49288