Theorem rspccva 3621

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062

This theorem is referenced by:  disjne  4455  n0snor2el  4833  seex  5644  preddowncl  6353  frpoins3g  6367  foelrn  7127  foelrnf  7128  caofid0l  7730  caofid0r  7731  caofid1  7732  caofid2  7733  onnseq  8384  odi  8617  omsmolem  8695  naddssim  8723  fvixp  8942  unblem1  9328  ordiso2  9555  unwdomg  9624  ac5num  10076  acni2  10086  fodomacn  10096  iundom2g  10580  fpwwe2lem3  10673  eltsk2g  10791  tskpwss  10792  tskpw  10793  tsken  10794  prlem934  11073  dedekindle  11425  ltord1  11789  leord1  11790  eqord1  11791  ltord2  11792  leord2  11793  eqord2  11794  supmul1  12237  seqcaopr2  14079  bccl  14361  hashbc  14492  limsupbnd2  15519  2clim  15608  climsup  15706  caurcvg2  15714  caucvgb  15716  isummulc2  15798  telfsumo2  15839  fsumparts  15842  incexclem  15872  isumshft  15875  climcndslem1  15885  climcndslem2  15886  supcvg  15892  geomulcvg  15912  mertenslem2  15921  mertens  15922  bpolycl  16088  bpolydif  16091  rpnnen2lem10  16259  dvdsprime  16724  fuciso  18023  lubub  18556  lubl  18557  mgmlrid  18680  grpinvalem  18686  grpinvex  18961  issubg2  19159  issubg4  19163  nmzbi  19182  gagrpid  19312  cntzi  19347  psgnunilem2  19513  sylow1lem3  19618  pgpfi  19623  slwispgp  19629  sylow2alem1  19635  dprdfcl  20033  ablfac2  20109  abveq0  20819  issrngd  20856  phllmhm  21650  ipcl  21651  ipeq0  21656  isphld  21672  ocvi  21687  pf1ind  22359  cayhamlem3  22893  elcls3  23091  neindisj2  23131  perfi  23163  cnima  23273  1stcfb  23453  1stcelcls  23469  llyi  23482  nllyi  23483  locfinnei  23531  1stckgenlem  23561  ptbasin  23585  txcls  23612  ptcnp  23630  ufli  23922  tgpt0  24127  tsmsxplem2  24162  nrmmetd  24587  tngngp  24675  tngngp3  24677  reperflem  24840  lebnumlem3  24995  htpyi  25006  htpycc  25012  phtpyi  25016  cfili  25302  cmetcvg  25319  caubl  25342  caublcls  25343  bcthlem2  25359  bcthlem3  25360  bcthlem4  25361  ovolicc2lem1  25552  ovolicc2lem5  25556  ovolicc2  25557  voliunlem3  25587  volsuplem  25590  uniioombllem2  25618  mbfima  25665  ismbfd  25674  ismbf3d  25689  mbfmullem  25760  itg2monolem1  25785  itg2i1fseqle  25789  itg2i1fseq  25790  itg2i1fseq2  25791  itg2addlem  25793  bddmulibl  25874  bddiblnc  25877  c1liplem1  26035  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumrlimf  26065  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlimge0  26071  dvfsum2  26075  ftc1lem6  26082  ulmcau  26438  ulmdvlem1  26443  ulmdvlem3  26445  mtestbdd  26448  itgulm  26451  radcnvlem1  26456  abelthlem5  26479  abelthlem7  26482  areambl  27001  2lgslem1a  27435  dchrisumlem2  27534  dchrvmasumiflem1  27545  pntpbnd1  27630  ostthlem1  27671  madebday  27938  addscom  27999  precsexlem9  28239  peano5n0s  28324  zs12bday  28424  tglowdim1i  28509  brbtwn2  28920  ax5seglem1  28943  ax5seglem2  28944  ax5seglem9  28952  axcontlem4  28982  axcontlem12  28990  fusgreghash2wsp  30357  grpoidinvlem3  30525  grpoidinv  30527  grpoidinv2  30534  vcidOLD  30583  minvecolem5  30900  hcaucvg  31205  hlimconvi  31210  lnopeq0i  32026  cnlnadjlem5  32090  csmdsymi  32353  difelsiga  34134  eulerpartlemb  34370  ballotlemfc0  34495  ballotlemfcc  34496  ptpconn  35238  cvmsdisj  35275  cvmshmeo  35276  snmlflim  35337  elmrsubrn  35525  mvtinf  35560  sinccvg  35678  fnemeet1  36367  fnemeet2  36368  fnejoin1  36369  fnejoin2  36370  bj-seex  36923  poimirlem27  37654  poimirlem32  37659  mblfinlem1  37664  ovoliunnfl  37669  ex-ovoliunnfl  37670  voliunnfl  37671  volsupnfl  37672  mbfresfi  37673  itg2gt0cn  37682  ftc1cnnc  37699  ftc1anc  37708  upixp  37736  filbcmb  37747  sdclem1  37750  seqpo  37754  incsequz2  37756  mettrifi  37764  caushft  37768  sstotbnd2  37781  heibor1lem  37816  heiborlem3  37820  heiborlem10  37827  heibor  37828  rrndstprj2  37838  cmpidelt  37866  rngoid  37909  fsuppind  42600  limsuc2  43053  cvgdvgrat  44332  cncmpmax  45037  mccllem  45612  mccl  45613  climinf  45621  climsuse  45623  islptre  45634  limcperiod  45643  addlimc  45663  0ellimcdiv  45664  cncficcgt0  45903  dvbdfbdioolem2  45944  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem3  45963  stoweidlem7  46022  stoweidlem15  46030  stoweidlem21  46036  stoweidlem31  46046  stoweidlem35  46050  stoweidlem36  46051  stoweidlem50  46065  stoweidlem57  46072  stoweidlem59  46074  wallispilem3  46082  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem32  46154  fourierdlem33  46155  fourierdlem39  46161  fourierdlem62  46183  fourierdlem71  46192  fourierdlem89  46210  fourierdlem91  46212  fourierdlem93  46214  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  etransclem24  46273  etransclem32  46281  smflimlem6  46791  smfpimcc  46823  smfsuplem2  46827  gricushgr  47886