Theorem rspccva 3620

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059

This theorem is referenced by:  disjne  4460  n0snor2el  4837  seex  5647  preddowncl  6354  frpoins3g  6368  foelrn  7126  foelrnf  7127  caofid0l  7729  caofid0r  7730  caofid1  7731  caofid2  7732  onnseq  8382  odi  8615  omsmolem  8693  naddssim  8721  fvixp  8940  unblem1  9325  ordiso2  9552  unwdomg  9621  ac5num  10073  acni2  10083  fodomacn  10093  iundom2g  10577  fpwwe2lem3  10670  eltsk2g  10788  tskpwss  10789  tskpw  10790  tsken  10791  prlem934  11070  dedekindle  11422  ltord1  11786  leord1  11787  eqord1  11788  ltord2  11789  leord2  11790  eqord2  11791  supmul1  12234  seqcaopr2  14075  bccl  14357  hashbc  14488  limsupbnd2  15515  2clim  15604  climsup  15702  caurcvg2  15710  caucvgb  15712  isummulc2  15794  telfsumo2  15835  fsumparts  15838  incexclem  15868  isumshft  15871  climcndslem1  15881  climcndslem2  15882  supcvg  15888  geomulcvg  15908  mertenslem2  15917  mertens  15918  bpolycl  16084  bpolydif  16087  rpnnen2lem10  16255  dvdsprime  16720  fuciso  18031  lubub  18568  lubl  18569  mgmlrid  18692  grpinvalem  18698  grpinvex  18973  issubg2  19171  issubg4  19175  nmzbi  19194  gagrpid  19324  cntzi  19359  psgnunilem2  19527  sylow1lem3  19632  pgpfi  19637  slwispgp  19643  sylow2alem1  19649  dprdfcl  20047  ablfac2  20123  abveq0  20835  issrngd  20872  phllmhm  21667  ipcl  21668  ipeq0  21673  isphld  21689  ocvi  21704  pf1ind  22374  cayhamlem3  22908  elcls3  23106  neindisj2  23146  perfi  23178  cnima  23288  1stcfb  23468  1stcelcls  23484  llyi  23497  nllyi  23498  locfinnei  23546  1stckgenlem  23576  ptbasin  23600  txcls  23627  ptcnp  23645  ufli  23937  tgpt0  24142  tsmsxplem2  24177  nrmmetd  24602  tngngp  24690  tngngp3  24692  reperflem  24853  lebnumlem3  25008  htpyi  25019  htpycc  25025  phtpyi  25029  cfili  25315  cmetcvg  25332  caubl  25355  caublcls  25356  bcthlem2  25372  bcthlem3  25373  bcthlem4  25374  ovolicc2lem1  25565  ovolicc2lem5  25569  ovolicc2  25570  voliunlem3  25600  volsuplem  25603  uniioombllem2  25631  mbfima  25678  ismbfd  25687  ismbf3d  25702  mbfmullem  25774  itg2monolem1  25799  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  bddmulibl  25888  bddiblnc  25891  c1liplem1  26049  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumrlimf  26079  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlimge0  26085  dvfsum2  26089  ftc1lem6  26096  ulmcau  26452  ulmdvlem1  26457  ulmdvlem3  26459  mtestbdd  26462  itgulm  26465  radcnvlem1  26470  abelthlem5  26493  abelthlem7  26496  areambl  27015  2lgslem1a  27449  dchrisumlem2  27548  dchrvmasumiflem1  27559  pntpbnd1  27644  ostthlem1  27685  madebday  27952  addscom  28013  precsexlem9  28253  peano5n0s  28338  zs12bday  28438  tglowdim1i  28523  brbtwn2  28934  ax5seglem1  28957  ax5seglem2  28958  ax5seglem9  28966  axcontlem4  28996  axcontlem12  29004  fusgreghash2wsp  30366  grpoidinvlem3  30534  grpoidinv  30536  grpoidinv2  30543  vcidOLD  30592  minvecolem5  30909  hcaucvg  31214  hlimconvi  31219  lnopeq0i  32035  cnlnadjlem5  32099  csmdsymi  32362  difelsiga  34113  eulerpartlemb  34349  ballotlemfc0  34473  ballotlemfcc  34474  ptpconn  35217  cvmsdisj  35254  cvmshmeo  35255  snmlflim  35316  elmrsubrn  35504  mvtinf  35539  sinccvg  35657  fnemeet1  36348  fnemeet2  36349  fnejoin1  36350  fnejoin2  36351  bj-seex  36904  poimirlem27  37633  poimirlem32  37638  mblfinlem1  37643  ovoliunnfl  37648  ex-ovoliunnfl  37649  voliunnfl  37650  volsupnfl  37651  mbfresfi  37652  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anc  37687  upixp  37715  filbcmb  37726  sdclem1  37729  seqpo  37733  incsequz2  37735  mettrifi  37743  caushft  37747  sstotbnd2  37760  heibor1lem  37795  heiborlem3  37799  heiborlem10  37806  heibor  37807  rrndstprj2  37817  cmpidelt  37845  rngoid  37888  fsuppind  42576  limsuc2  43029  cvgdvgrat  44308  cncmpmax  44969  mccllem  45552  mccl  45553  climinf  45561  climsuse  45563  islptre  45574  limcperiod  45583  addlimc  45603  0ellimcdiv  45604  cncficcgt0  45843  dvbdfbdioolem2  45884  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem3  45903  stoweidlem7  45962  stoweidlem15  45970  stoweidlem21  45976  stoweidlem31  45986  stoweidlem35  45990  stoweidlem36  45991  stoweidlem50  46005  stoweidlem57  46012  stoweidlem59  46014  wallispilem3  46022  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem32  46094  fourierdlem33  46095  fourierdlem39  46101  fourierdlem62  46123  fourierdlem71  46132  fourierdlem89  46150  fourierdlem91  46152  fourierdlem93  46154  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  etransclem24  46213  etransclem32  46221  smflimlem6  46731  smfpimcc  46763  smfsuplem2  46767  gricushgr  47823