Theorem rspccva 3551

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068

This theorem is referenced by:  disjne  4385  n0snor2el  4761  seex  5542  preddowncl  6224  frpoins3g  6234  foelrn  6964  caofid0l  7542  caofid0r  7543  caofid1  7544  caofid2  7545  onnseq  8146  odi  8372  omsmolem  8447  fvixp  8648  unblem1  8996  ordiso2  9204  unwdomg  9273  ac5num  9723  acni2  9733  fodomacn  9743  iundom2g  10227  fpwwe2lem3  10320  eltsk2g  10438  tskpwss  10439  tskpw  10440  tsken  10441  prlem934  10720  dedekindle  11069  ltord1  11431  leord1  11432  eqord1  11433  ltord2  11434  leord2  11435  eqord2  11436  supmul1  11874  seqcaopr2  13687  bccl  13964  hashbc  14093  limsupbnd2  15120  2clim  15209  climsup  15309  caurcvg2  15317  caucvgb  15319  isummulc2  15402  telfsumo2  15443  fsumparts  15446  incexclem  15476  isumshft  15479  climcndslem1  15489  climcndslem2  15490  supcvg  15496  geomulcvg  15516  mertenslem2  15525  mertens  15526  bpolycl  15690  bpolydif  15693  rpnnen2lem10  15860  dvdsprime  16320  fuciso  17609  lubub  18144  lubl  18145  mgmlrid  18266  grprinvlem  18272  grpinvex  18502  issubg2  18685  issubg4  18689  nmzbi  18707  gagrpid  18815  cntzi  18850  psgnunilem2  19018  sylow1lem3  19120  pgpfi  19125  slwispgp  19131  sylow2alem1  19137  dprdfcl  19531  ablfac2  19607  abveq0  20001  issrngd  20036  phllmhm  20749  ipcl  20750  ipeq0  20755  isphld  20771  ocvi  20786  psrbagconf1oOLD  21050  pf1ind  21431  cayhamlem3  21944  elcls3  22142  neindisj2  22182  perfi  22214  cnima  22324  1stcfb  22504  1stcelcls  22520  llyi  22533  nllyi  22534  locfinnei  22582  1stckgenlem  22612  ptbasin  22636  txcls  22663  ptcnp  22681  ufli  22973  tgpt0  23178  tsmsxplem2  23213  nrmmetd  23636  tngngp  23724  tngngp3  23726  reperflem  23887  lebnumlem3  24032  htpyi  24043  htpycc  24049  phtpyi  24053  cfili  24337  cmetcvg  24354  caubl  24377  caublcls  24378  bcthlem2  24394  bcthlem3  24395  bcthlem4  24396  ovolicc2lem1  24586  ovolicc2lem5  24590  ovolicc2  24591  voliunlem3  24621  volsuplem  24624  uniioombllem2  24652  mbfima  24699  ismbfd  24708  ismbf3d  24723  mbfmullem  24795  itg2monolem1  24820  itg2i1fseqle  24824  itg2i1fseq  24825  itg2i1fseq2  24826  itg2addlem  24828  bddmulibl  24908  bddiblnc  24911  c1liplem1  25065  dvfsumle  25090  dvfsumabs  25092  dvfsumrlimf  25094  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsumrlimge0  25099  dvfsum2  25103  ftc1lem6  25110  ulmcau  25459  ulmdvlem1  25464  ulmdvlem3  25466  mtestbdd  25469  itgulm  25472  radcnvlem1  25477  abelthlem5  25499  abelthlem7  25502  areambl  26013  2lgslem1a  26444  dchrisumlem2  26543  dchrvmasumiflem1  26554  pntpbnd1  26639  ostthlem1  26680  tglowdim1i  26766  brbtwn2  27176  ax5seglem1  27199  ax5seglem2  27200  ax5seglem9  27208  axcontlem4  27238  axcontlem12  27246  fusgreghash2wsp  28603  grpoidinvlem3  28769  grpoidinv  28771  grpoidinv2  28778  vcidOLD  28827  minvecolem5  29144  hcaucvg  29449  hlimconvi  29454  lnopeq0i  30270  cnlnadjlem5  30334  csmdsymi  30597  difelsiga  32001  eulerpartlemb  32235  ballotlemfc0  32359  ballotlemfcc  32360  ptpconn  33095  cvmsdisj  33132  cvmshmeo  33133  snmlflim  33194  elmrsubrn  33382  mvtinf  33417  sinccvg  33531  naddssim  33764  madebday  34007  addscom  34056  fnemeet1  34482  fnemeet2  34483  fnejoin1  34484  fnejoin2  34485  bj-seex  35037  poimirlem27  35731  poimirlem32  35736  mblfinlem1  35741  ovoliunnfl  35746  ex-ovoliunnfl  35747  voliunnfl  35748  volsupnfl  35749  mbfresfi  35750  itg2gt0cn  35759  ftc1cnnc  35776  ftc1anc  35785  upixp  35814  filbcmb  35825  sdclem1  35828  seqpo  35832  incsequz2  35834  mettrifi  35842  caushft  35846  sstotbnd2  35859  heibor1lem  35894  heiborlem3  35898  heiborlem10  35905  heibor  35906  rrndstprj2  35916  cmpidelt  35944  rngoid  35987  fsuppind  40202  limsuc2  40782  cvgdvgrat  41820  cncmpmax  42464  foelrnf  42613  mccllem  43028  mccl  43029  climinf  43037  climsuse  43039  islptre  43050  limcperiod  43059  addlimc  43079  0ellimcdiv  43080  cncficcgt0  43319  dvbdfbdioolem2  43360  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem3  43379  stoweidlem7  43438  stoweidlem15  43446  stoweidlem21  43452  stoweidlem31  43462  stoweidlem35  43466  stoweidlem36  43467  stoweidlem50  43481  stoweidlem57  43488  stoweidlem59  43490  wallispilem3  43498  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem32  43570  fourierdlem33  43571  fourierdlem39  43577  fourierdlem62  43599  fourierdlem71  43608  fourierdlem89  43626  fourierdlem91  43628  fourierdlem93  43630  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  etransclem24  43689  etransclem32  43697  smflimlem6  44198  smfpimcc  44228  smfsuplem2  44232  isomushgr  45166