Theorem rspccva 3559

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069

This theorem is referenced by:  disjne  4389  n0snor2el  4765  seex  5547  preddowncl  6229  frpoins3g  6243  foelrn  6975  caofid0l  7555  caofid0r  7556  caofid1  7557  caofid2  7558  onnseq  8163  odi  8398  omsmolem  8475  fvixp  8678  unblem1  9054  ordiso2  9262  unwdomg  9331  ac5num  9780  acni2  9790  fodomacn  9800  iundom2g  10284  fpwwe2lem3  10377  eltsk2g  10495  tskpwss  10496  tskpw  10497  tsken  10498  prlem934  10777  dedekindle  11127  ltord1  11489  leord1  11490  eqord1  11491  ltord2  11492  leord2  11493  eqord2  11494  supmul1  11932  seqcaopr2  13747  bccl  14024  hashbc  14153  limsupbnd2  15180  2clim  15269  climsup  15369  caurcvg2  15377  caucvgb  15379  isummulc2  15462  telfsumo2  15503  fsumparts  15506  incexclem  15536  isumshft  15539  climcndslem1  15549  climcndslem2  15550  supcvg  15556  geomulcvg  15576  mertenslem2  15585  mertens  15586  bpolycl  15750  bpolydif  15753  rpnnen2lem10  15920  dvdsprime  16380  fuciso  17681  lubub  18217  lubl  18218  mgmlrid  18339  grprinvlem  18345  grpinvex  18575  issubg2  18758  issubg4  18762  nmzbi  18780  gagrpid  18888  cntzi  18923  psgnunilem2  19091  sylow1lem3  19193  pgpfi  19198  slwispgp  19204  sylow2alem1  19210  dprdfcl  19604  ablfac2  19680  abveq0  20074  issrngd  20109  phllmhm  20825  ipcl  20826  ipeq0  20831  isphld  20847  ocvi  20862  psrbagconf1oOLD  21128  pf1ind  21509  cayhamlem3  22024  elcls3  22222  neindisj2  22262  perfi  22294  cnima  22404  1stcfb  22584  1stcelcls  22600  llyi  22613  nllyi  22614  locfinnei  22662  1stckgenlem  22692  ptbasin  22716  txcls  22743  ptcnp  22761  ufli  23053  tgpt0  23258  tsmsxplem2  23293  nrmmetd  23718  tngngp  23806  tngngp3  23808  reperflem  23969  lebnumlem3  24114  htpyi  24125  htpycc  24131  phtpyi  24135  cfili  24420  cmetcvg  24437  caubl  24460  caublcls  24461  bcthlem2  24477  bcthlem3  24478  bcthlem4  24479  ovolicc2lem1  24669  ovolicc2lem5  24673  ovolicc2  24674  voliunlem3  24704  volsuplem  24707  uniioombllem2  24735  mbfima  24782  ismbfd  24791  ismbf3d  24806  mbfmullem  24878  itg2monolem1  24903  itg2i1fseqle  24907  itg2i1fseq  24908  itg2i1fseq2  24909  itg2addlem  24911  bddmulibl  24991  bddiblnc  24994  c1liplem1  25148  dvfsumle  25173  dvfsumabs  25175  dvfsumrlimf  25177  dvfsumlem1  25178  dvfsumlem2  25179  dvfsumlem3  25180  dvfsumlem4  25181  dvfsumrlimge0  25182  dvfsum2  25186  ftc1lem6  25193  ulmcau  25542  ulmdvlem1  25547  ulmdvlem3  25549  mtestbdd  25552  itgulm  25555  radcnvlem1  25560  abelthlem5  25582  abelthlem7  25585  areambl  26096  2lgslem1a  26527  dchrisumlem2  26626  dchrvmasumiflem1  26637  pntpbnd1  26722  ostthlem1  26763  tglowdim1i  26850  brbtwn2  27261  ax5seglem1  27284  ax5seglem2  27285  ax5seglem9  27293  axcontlem4  27323  axcontlem12  27331  fusgreghash2wsp  28688  grpoidinvlem3  28854  grpoidinv  28856  grpoidinv2  28863  vcidOLD  28912  minvecolem5  29229  hcaucvg  29534  hlimconvi  29539  lnopeq0i  30355  cnlnadjlem5  30419  csmdsymi  30682  difelsiga  32087  eulerpartlemb  32321  ballotlemfc0  32445  ballotlemfcc  32446  ptpconn  33181  cvmsdisj  33218  cvmshmeo  33219  snmlflim  33280  elmrsubrn  33468  mvtinf  33503  sinccvg  33617  naddssim  33823  madebday  34066  addscom  34115  fnemeet1  34541  fnemeet2  34542  fnejoin1  34543  fnejoin2  34544  bj-seex  35096  poimirlem27  35790  poimirlem32  35795  mblfinlem1  35800  ovoliunnfl  35805  ex-ovoliunnfl  35806  voliunnfl  35807  volsupnfl  35808  mbfresfi  35809  itg2gt0cn  35818  ftc1cnnc  35835  ftc1anc  35844  upixp  35873  filbcmb  35884  sdclem1  35887  seqpo  35891  incsequz2  35893  mettrifi  35901  caushft  35905  sstotbnd2  35918  heibor1lem  35953  heiborlem3  35957  heiborlem10  35964  heibor  35965  rrndstprj2  35975  cmpidelt  36003  rngoid  36046  fsuppind  40265  limsuc2  40852  cvgdvgrat  41890  cncmpmax  42534  foelrnf  42683  mccllem  43097  mccl  43098  climinf  43106  climsuse  43108  islptre  43119  limcperiod  43128  addlimc  43148  0ellimcdiv  43149  cncficcgt0  43388  dvbdfbdioolem2  43429  ioodvbdlimc1lem2  43432  ioodvbdlimc2lem  43434  dvnprodlem3  43448  stoweidlem7  43507  stoweidlem15  43515  stoweidlem21  43521  stoweidlem31  43531  stoweidlem35  43535  stoweidlem36  43536  stoweidlem50  43550  stoweidlem57  43557  stoweidlem59  43559  wallispilem3  43567  dirkercncflem2  43604  dirkercncflem4  43606  fourierdlem32  43639  fourierdlem33  43640  fourierdlem39  43646  fourierdlem62  43668  fourierdlem71  43677  fourierdlem89  43695  fourierdlem91  43697  fourierdlem93  43699  fourierdlem101  43707  fourierdlem103  43709  fourierdlem104  43710  etransclem24  43758  etransclem32  43766  smflimlem6  44267  smfpimcc  44297  smfsuplem2  44301  isomushgr  45234