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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  disjne  4384  n0snor2el  4765  seex  5578  preddowncl  6284  frpoins3g  6298  foelrn  7049  foelrnf  7050  caofid0l  7654  caofid0r  7655  caofid1  7656  caofid2  7657  onnseq  8275  odi  8505  omsmolem  8584  naddssim  8612  fvixp  8841  unblem1  9193  ordiso2  9421  unwdomg  9490  ac5num  9950  acni2  9960  fodomacn  9970  iundom2g  10454  fpwwe2lem3  10548  eltsk2g  10666  tskpwss  10667  tskpw  10668  tsken  10669  prlem934  10948  dedekindle  11302  ltord1  11668  leord1  11669  eqord1  11670  ltord2  11671  leord2  11672  eqord2  11673  supmul1  12117  seqcaopr2  13992  bccl  14276  hashbc  14407  limsupbnd2  15437  2clim  15526  climsup  15624  caurcvg2  15632  caucvgb  15634  isummulc2  15716  telfsumo2  15758  fsumparts  15761  incexclem  15793  isumshft  15796  climcndslem1  15806  climcndslem2  15807  supcvg  15813  geomulcvg  15833  mertenslem2  15842  mertens  15843  bpolycl  16009  bpolydif  16012  rpnnen2lem10  16182  dvdsprime  16648  fuciso  17937  lubub  18469  lubl  18470  mgmlrid  18627  grpinvalem  18633  grpinvex  18911  issubg2  19109  issubg4  19113  nmzbi  19131  gagrpid  19261  cntzi  19296  psgnunilem2  19462  sylow1lem3  19567  pgpfi  19572  slwispgp  19578  sylow2alem1  19584  dprdfcl  19982  ablfac2  20058  abveq0  20791  issrngd  20828  phllmhm  21608  ipcl  21609  ipeq0  21614  isphld  21630  ocvi  21645  pf1ind  22342  cayhamlem3  22871  elcls3  23067  neindisj2  23107  perfi  23139  cnima  23249  1stcfb  23429  1stcelcls  23445  llyi  23458  nllyi  23459  locfinnei  23507  1stckgenlem  23537  ptbasin  23561  txcls  23588  ptcnp  23606  ufli  23898  tgpt0  24103  tsmsxplem2  24138  nrmmetd  24558  tngngp  24638  tngngp3  24640  reperflem  24803  lebnumlem3  24949  htpyi  24960  htpycc  24966  phtpyi  24970  cfili  25254  cmetcvg  25271  caubl  25294  caublcls  25295  bcthlem2  25311  bcthlem3  25312  bcthlem4  25313  ovolicc2lem1  25503  ovolicc2lem5  25507  ovolicc2  25508  voliunlem3  25538  volsuplem  25541  uniioombllem2  25569  mbfima  25616  ismbfd  25625  ismbf3d  25640  mbfmullem  25711  itg2monolem1  25736  itg2i1fseqle  25740  itg2i1fseq  25741  itg2i1fseq2  25742  itg2addlem  25744  bddmulibl  25825  bddiblnc  25828  c1liplem1  25982  dvfsumle  26007  dvfsumabs  26009  dvfsumrlimf  26011  dvfsumlem1  26012  dvfsumlem2  26013  dvfsumlem3  26014  dvfsumlem4  26015  dvfsumrlimge0  26016  dvfsum2  26020  ftc1lem6  26027  ulmcau  26379  ulmdvlem1  26384  ulmdvlem3  26386  mtestbdd  26389  itgulm  26392  radcnvlem1  26397  abelthlem5  26419  abelthlem7  26422  areambl  26941  2lgslem1a  27373  dchrisumlem2  27472  dchrvmasumiflem1  27483  pntpbnd1  27568  ostthlem1  27609  madebday  27911  addscom  27977  precsexlem9  28226  peano5n0s  28330  bdayfinbndlem1  28478  tglowdim1i  28588  brbtwn2  28993  ax5seglem1  29016  ax5seglem2  29017  ax5seglem9  29025  axcontlem4  29055  axcontlem12  29063  fusgreghash2wsp  30427  grpoidinvlem3  30596  grpoidinv  30598  grpoidinv2  30605  vcidOLD  30654  minvecolem5  30971  hcaucvg  31276  hlimconvi  31281  lnopeq0i  32097  cnlnadjlem5  32161  csmdsymi  32424  difelsiga  34326  eulerpartlemb  34561  ballotlemfc0  34686  ballotlemfcc  34687  ptpconn  35470  cvmsdisj  35507  cvmshmeo  35508  snmlflim  35569  elmrsubrn  35757  mvtinf  35792  sinccvg  35910  fnemeet1  36603  fnemeet2  36604  fnejoin1  36605  fnejoin2  36606  bj-seex  37284  poimirlem27  38023  poimirlem32  38028  mblfinlem1  38033  ovoliunnfl  38038  ex-ovoliunnfl  38039  voliunnfl  38040  volsupnfl  38041  mbfresfi  38042  itg2gt0cn  38051  ftc1cnnc  38068  ftc1anc  38077  upixp  38105  filbcmb  38116  sdclem1  38119  seqpo  38123  incsequz2  38125  mettrifi  38133  caushft  38137  sstotbnd2  38150  heibor1lem  38185  heiborlem3  38189  heiborlem10  38196  heibor  38197  rrndstprj2  38207  cmpidelt  38235  rngoid  38278  fsuppind  43049  limsuc2  43495  cvgdvgrat  44766  cncmpmax  45489  mccllem  46050  mccl  46051  climinf  46059  climsuse  46061  islptre  46072  limcperiod  46081  addlimc  46099  0ellimcdiv  46100  cncficcgt0  46339  dvbdfbdioolem2  46380  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  dvnprodlem3  46399  stoweidlem7  46458  stoweidlem15  46466  stoweidlem21  46472  stoweidlem31  46482  stoweidlem35  46486  stoweidlem36  46487  stoweidlem50  46501  stoweidlem57  46508  stoweidlem59  46510  wallispilem3  46518  dirkercncflem2  46555  dirkercncflem4  46557  fourierdlem32  46590  fourierdlem33  46591  fourierdlem39  46597  fourierdlem62  46619  fourierdlem71  46628  fourierdlem89  46646  fourierdlem91  46648  fourierdlem93  46650  fourierdlem101  46658  fourierdlem103  46660  fourierdlem104  46661  etransclem24  46709  etransclem32  46717  smflimlem6  47227  smfpimcc  47259  smfsuplem2  47263  gricushgr  48416