Theorem rspccva 3634

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  disjne  4478  n0snor2el  4858  seex  5659  preddowncl  6364  frpoins3g  6378  foelrn  7141  foelrnf  7142  caofid0l  7746  caofid0r  7747  caofid1  7748  caofid2  7749  onnseq  8400  odi  8635  omsmolem  8713  naddssim  8741  fvixp  8960  unblem1  9356  ordiso2  9584  unwdomg  9653  ac5num  10105  acni2  10115  fodomacn  10125  iundom2g  10609  fpwwe2lem3  10702  eltsk2g  10820  tskpwss  10821  tskpw  10822  tsken  10823  prlem934  11102  dedekindle  11454  ltord1  11816  leord1  11817  eqord1  11818  ltord2  11819  leord2  11820  eqord2  11821  supmul1  12264  seqcaopr2  14089  bccl  14371  hashbc  14502  limsupbnd2  15529  2clim  15618  climsup  15718  caurcvg2  15726  caucvgb  15728  isummulc2  15810  telfsumo2  15851  fsumparts  15854  incexclem  15884  isumshft  15887  climcndslem1  15897  climcndslem2  15898  supcvg  15904  geomulcvg  15924  mertenslem2  15933  mertens  15934  bpolycl  16100  bpolydif  16103  rpnnen2lem10  16271  dvdsprime  16734  fuciso  18045  lubub  18581  lubl  18582  mgmlrid  18705  grpinvalem  18711  grpinvex  18983  issubg2  19181  issubg4  19185  nmzbi  19204  gagrpid  19334  cntzi  19369  psgnunilem2  19537  sylow1lem3  19642  pgpfi  19647  slwispgp  19653  sylow2alem1  19659  dprdfcl  20057  ablfac2  20133  abveq0  20841  issrngd  20878  phllmhm  21673  ipcl  21674  ipeq0  21679  isphld  21695  ocvi  21710  pf1ind  22380  cayhamlem3  22914  elcls3  23112  neindisj2  23152  perfi  23184  cnima  23294  1stcfb  23474  1stcelcls  23490  llyi  23503  nllyi  23504  locfinnei  23552  1stckgenlem  23582  ptbasin  23606  txcls  23633  ptcnp  23651  ufli  23943  tgpt0  24148  tsmsxplem2  24183  nrmmetd  24608  tngngp  24696  tngngp3  24698  reperflem  24859  lebnumlem3  25014  htpyi  25025  htpycc  25031  phtpyi  25035  cfili  25321  cmetcvg  25338  caubl  25361  caublcls  25362  bcthlem2  25378  bcthlem3  25379  bcthlem4  25380  ovolicc2lem1  25571  ovolicc2lem5  25575  ovolicc2  25576  voliunlem3  25606  volsuplem  25609  uniioombllem2  25637  mbfima  25684  ismbfd  25693  ismbf3d  25708  mbfmullem  25780  itg2monolem1  25805  itg2i1fseqle  25809  itg2i1fseq  25810  itg2i1fseq2  25811  itg2addlem  25813  bddmulibl  25894  bddiblnc  25897  c1liplem1  26055  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumrlimf  26085  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlimge0  26091  dvfsum2  26095  ftc1lem6  26102  ulmcau  26456  ulmdvlem1  26461  ulmdvlem3  26463  mtestbdd  26466  itgulm  26469  radcnvlem1  26474  abelthlem5  26497  abelthlem7  26500  areambl  27019  2lgslem1a  27453  dchrisumlem2  27552  dchrvmasumiflem1  27563  pntpbnd1  27648  ostthlem1  27689  madebday  27956  addscom  28017  precsexlem9  28257  peano5n0s  28342  zs12bday  28442  tglowdim1i  28527  brbtwn2  28938  ax5seglem1  28961  ax5seglem2  28962  ax5seglem9  28970  axcontlem4  29000  axcontlem12  29008  fusgreghash2wsp  30370  grpoidinvlem3  30538  grpoidinv  30540  grpoidinv2  30547  vcidOLD  30596  minvecolem5  30913  hcaucvg  31218  hlimconvi  31223  lnopeq0i  32039  cnlnadjlem5  32103  csmdsymi  32366  difelsiga  34097  eulerpartlemb  34333  ballotlemfc0  34457  ballotlemfcc  34458  ptpconn  35201  cvmsdisj  35238  cvmshmeo  35239  snmlflim  35300  elmrsubrn  35488  mvtinf  35523  sinccvg  35641  fnemeet1  36332  fnemeet2  36333  fnejoin1  36334  fnejoin2  36335  bj-seex  36888  poimirlem27  37607  poimirlem32  37612  mblfinlem1  37617  ovoliunnfl  37622  ex-ovoliunnfl  37623  voliunnfl  37624  volsupnfl  37625  mbfresfi  37626  itg2gt0cn  37635  ftc1cnnc  37652  ftc1anc  37661  upixp  37689  filbcmb  37700  sdclem1  37703  seqpo  37707  incsequz2  37709  mettrifi  37717  caushft  37721  sstotbnd2  37734  heibor1lem  37769  heiborlem3  37773  heiborlem10  37780  heibor  37781  rrndstprj2  37791  cmpidelt  37819  rngoid  37862  fsuppind  42545  limsuc2  42998  cvgdvgrat  44282  cncmpmax  44932  mccllem  45518  mccl  45519  climinf  45527  climsuse  45529  islptre  45540  limcperiod  45549  addlimc  45569  0ellimcdiv  45570  cncficcgt0  45809  dvbdfbdioolem2  45850  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem3  45869  stoweidlem7  45928  stoweidlem15  45936  stoweidlem21  45942  stoweidlem31  45952  stoweidlem35  45956  stoweidlem36  45957  stoweidlem50  45971  stoweidlem57  45978  stoweidlem59  45980  wallispilem3  45988  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem32  46060  fourierdlem33  46061  fourierdlem39  46067  fourierdlem62  46089  fourierdlem71  46098  fourierdlem89  46116  fourierdlem91  46118  fourierdlem93  46120  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  etransclem24  46179  etransclem32  46187  smflimlem6  46697  smfpimcc  46729  smfsuplem2  46733  gricushgr  47770