Theorem rspccva 3573

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050

This theorem is referenced by:  disjne  4405  n0snor2el  4787  seex  5581  preddowncl  6288  frpoins3g  6302  foelrn  7050  foelrnf  7051  caofid0l  7653  caofid0r  7654  caofid1  7655  caofid2  7656  onnseq  8274  odi  8504  omsmolem  8583  naddssim  8611  fvixp  8838  unblem1  9190  ordiso2  9418  unwdomg  9487  ac5num  9944  acni2  9954  fodomacn  9964  iundom2g  10448  fpwwe2lem3  10542  eltsk2g  10660  tskpwss  10661  tskpw  10662  tsken  10663  prlem934  10942  dedekindle  11295  ltord1  11661  leord1  11662  eqord1  11663  ltord2  11664  leord2  11665  eqord2  11666  supmul1  12109  seqcaopr2  13959  bccl  14243  hashbc  14374  limsupbnd2  15404  2clim  15493  climsup  15591  caurcvg2  15599  caucvgb  15601  isummulc2  15683  telfsumo2  15724  fsumparts  15727  incexclem  15757  isumshft  15760  climcndslem1  15770  climcndslem2  15771  supcvg  15777  geomulcvg  15797  mertenslem2  15806  mertens  15807  bpolycl  15973  bpolydif  15976  rpnnen2lem10  16146  dvdsprime  16612  fuciso  17900  lubub  18432  lubl  18433  mgmlrid  18590  grpinvalem  18596  grpinvex  18871  issubg2  19069  issubg4  19073  nmzbi  19091  gagrpid  19221  cntzi  19256  psgnunilem2  19422  sylow1lem3  19527  pgpfi  19532  slwispgp  19538  sylow2alem1  19544  dprdfcl  19942  ablfac2  20018  abveq0  20749  issrngd  20786  phllmhm  21585  ipcl  21586  ipeq0  21591  isphld  21607  ocvi  21622  pf1ind  22297  cayhamlem3  22829  elcls3  23025  neindisj2  23065  perfi  23097  cnima  23207  1stcfb  23387  1stcelcls  23403  llyi  23416  nllyi  23417  locfinnei  23465  1stckgenlem  23495  ptbasin  23519  txcls  23546  ptcnp  23564  ufli  23856  tgpt0  24061  tsmsxplem2  24096  nrmmetd  24516  tngngp  24596  tngngp3  24598  reperflem  24761  lebnumlem3  24916  htpyi  24927  htpycc  24933  phtpyi  24937  cfili  25222  cmetcvg  25239  caubl  25262  caublcls  25263  bcthlem2  25279  bcthlem3  25280  bcthlem4  25281  ovolicc2lem1  25472  ovolicc2lem5  25476  ovolicc2  25477  voliunlem3  25507  volsuplem  25510  uniioombllem2  25538  mbfima  25585  ismbfd  25594  ismbf3d  25609  mbfmullem  25680  itg2monolem1  25705  itg2i1fseqle  25709  itg2i1fseq  25710  itg2i1fseq2  25711  itg2addlem  25713  bddmulibl  25794  bddiblnc  25797  c1liplem1  25955  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  dvfsumrlimf  25985  dvfsumlem1  25986  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem3  25989  dvfsumlem4  25990  dvfsumrlimge0  25991  dvfsum2  25995  ftc1lem6  26002  ulmcau  26358  ulmdvlem1  26363  ulmdvlem3  26365  mtestbdd  26368  itgulm  26371  radcnvlem1  26376  abelthlem5  26399  abelthlem7  26402  areambl  26922  2lgslem1a  27356  dchrisumlem2  27455  dchrvmasumiflem1  27466  pntpbnd1  27551  ostthlem1  27592  madebday  27872  addscom  27936  precsexlem9  28183  peano5n0s  28280  zs12bday  28433  tglowdim1i  28522  brbtwn2  28927  ax5seglem1  28950  ax5seglem2  28951  ax5seglem9  28959  axcontlem4  28989  axcontlem12  28997  fusgreghash2wsp  30362  grpoidinvlem3  30530  grpoidinv  30532  grpoidinv2  30539  vcidOLD  30588  minvecolem5  30905  hcaucvg  31210  hlimconvi  31215  lnopeq0i  32031  cnlnadjlem5  32095  csmdsymi  32358  difelsiga  34239  eulerpartlemb  34474  ballotlemfc0  34599  ballotlemfcc  34600  ptpconn  35376  cvmsdisj  35413  cvmshmeo  35414  snmlflim  35475  elmrsubrn  35663  mvtinf  35698  sinccvg  35816  fnemeet1  36509  fnemeet2  36510  fnejoin1  36511  fnejoin2  36512  bj-seex  37066  poimirlem27  37787  poimirlem32  37792  mblfinlem1  37797  ovoliunnfl  37802  ex-ovoliunnfl  37803  voliunnfl  37804  volsupnfl  37805  mbfresfi  37806  itg2gt0cn  37815  ftc1cnnc  37832  ftc1anc  37841  upixp  37869  filbcmb  37880  sdclem1  37883  seqpo  37887  incsequz2  37889  mettrifi  37897  caushft  37901  sstotbnd2  37914  heibor1lem  37949  heiborlem3  37953  heiborlem10  37960  heibor  37961  rrndstprj2  37971  cmpidelt  37999  rngoid  38042  fsuppind  42775  limsuc2  43225  cvgdvgrat  44496  cncmpmax  45219  mccllem  45785  mccl  45786  climinf  45794  climsuse  45796  islptre  45807  limcperiod  45816  addlimc  45834  0ellimcdiv  45835  cncficcgt0  46074  dvbdfbdioolem2  46115  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnprodlem3  46134  stoweidlem7  46193  stoweidlem15  46201  stoweidlem21  46207  stoweidlem31  46217  stoweidlem35  46221  stoweidlem36  46222  stoweidlem50  46236  stoweidlem57  46243  stoweidlem59  46245  wallispilem3  46253  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem32  46325  fourierdlem33  46326  fourierdlem39  46332  fourierdlem62  46354  fourierdlem71  46363  fourierdlem89  46381  fourierdlem91  46383  fourierdlem93  46385  fourierdlem101  46393  fourierdlem103  46395  fourierdlem104  46396  etransclem24  46444  etransclem32  46452  smflimlem6  46962  smfpimcc  46994  smfsuplem2  46998  gricushgr  48105