Theorem rspccva 3612

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  disjne  4455  n0snor2el  4835  seex  5639  preddowncl  6334  frpoins3g  6348  foelrn  7108  caofid0l  7701  caofid0r  7702  caofid1  7703  caofid2  7704  onnseq  8344  odi  8579  omsmolem  8656  naddssim  8684  fvixp  8896  unblem1  9295  ordiso2  9510  unwdomg  9579  ac5num  10031  acni2  10041  fodomacn  10051  iundom2g  10535  fpwwe2lem3  10628  eltsk2g  10746  tskpwss  10747  tskpw  10748  tsken  10749  prlem934  11028  dedekindle  11378  ltord1  11740  leord1  11741  eqord1  11742  ltord2  11743  leord2  11744  eqord2  11745  supmul1  12183  seqcaopr2  14004  bccl  14282  hashbc  14412  limsupbnd2  15427  2clim  15516  climsup  15616  caurcvg2  15624  caucvgb  15626  isummulc2  15708  telfsumo2  15749  fsumparts  15752  incexclem  15782  isumshft  15785  climcndslem1  15795  climcndslem2  15796  supcvg  15802  geomulcvg  15822  mertenslem2  15831  mertens  15832  bpolycl  15996  bpolydif  15999  rpnnen2lem10  16166  dvdsprime  16624  fuciso  17928  lubub  18464  lubl  18465  mgmlrid  18586  grprinvlem  18592  grpinvex  18829  issubg2  19021  issubg4  19025  nmzbi  19044  gagrpid  19158  cntzi  19193  psgnunilem2  19363  sylow1lem3  19468  pgpfi  19473  slwispgp  19479  sylow2alem1  19485  dprdfcl  19883  ablfac2  19959  abveq0  20434  issrngd  20469  phllmhm  21185  ipcl  21186  ipeq0  21191  isphld  21207  ocvi  21222  psrbagconf1oOLD  21490  pf1ind  21874  cayhamlem3  22389  elcls3  22587  neindisj2  22627  perfi  22659  cnima  22769  1stcfb  22949  1stcelcls  22965  llyi  22978  nllyi  22979  locfinnei  23027  1stckgenlem  23057  ptbasin  23081  txcls  23108  ptcnp  23126  ufli  23418  tgpt0  23623  tsmsxplem2  23658  nrmmetd  24083  tngngp  24171  tngngp3  24173  reperflem  24334  lebnumlem3  24479  htpyi  24490  htpycc  24496  phtpyi  24500  cfili  24785  cmetcvg  24802  caubl  24825  caublcls  24826  bcthlem2  24842  bcthlem3  24843  bcthlem4  24844  ovolicc2lem1  25034  ovolicc2lem5  25038  ovolicc2  25039  voliunlem3  25069  volsuplem  25072  uniioombllem2  25100  mbfima  25147  ismbfd  25156  ismbf3d  25171  mbfmullem  25243  itg2monolem1  25268  itg2i1fseqle  25272  itg2i1fseq  25273  itg2i1fseq2  25274  itg2addlem  25276  bddmulibl  25356  bddiblnc  25359  c1liplem1  25513  dvfsumle  25538  dvfsumabs  25540  dvfsumrlimf  25542  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlimge0  25547  dvfsum2  25551  ftc1lem6  25558  ulmcau  25907  ulmdvlem1  25912  ulmdvlem3  25914  mtestbdd  25917  itgulm  25920  radcnvlem1  25925  abelthlem5  25947  abelthlem7  25950  areambl  26463  2lgslem1a  26894  dchrisumlem2  26993  dchrvmasumiflem1  27004  pntpbnd1  27089  ostthlem1  27130  madebday  27395  addscom  27452  precsexlem9  27664  tglowdim1i  27783  brbtwn2  28194  ax5seglem1  28217  ax5seglem2  28218  ax5seglem9  28226  axcontlem4  28256  axcontlem12  28264  fusgreghash2wsp  29622  grpoidinvlem3  29790  grpoidinv  29792  grpoidinv2  29799  vcidOLD  29848  minvecolem5  30165  hcaucvg  30470  hlimconvi  30475  lnopeq0i  31291  cnlnadjlem5  31355  csmdsymi  31618  difelsiga  33162  eulerpartlemb  33398  ballotlemfc0  33522  ballotlemfcc  33523  ptpconn  34255  cvmsdisj  34292  cvmshmeo  34293  snmlflim  34354  elmrsubrn  34542  mvtinf  34577  sinccvg  34689  gg-dvfsumle  35213  gg-dvfsumlem2  35214  fnemeet1  35299  fnemeet2  35300  fnejoin1  35301  fnejoin2  35302  bj-seex  35850  poimirlem27  36563  poimirlem32  36568  mblfinlem1  36573  ovoliunnfl  36578  ex-ovoliunnfl  36579  voliunnfl  36580  volsupnfl  36581  mbfresfi  36582  itg2gt0cn  36591  ftc1cnnc  36608  ftc1anc  36617  upixp  36645  filbcmb  36656  sdclem1  36659  seqpo  36663  incsequz2  36665  mettrifi  36673  caushft  36677  sstotbnd2  36690  heibor1lem  36725  heiborlem3  36729  heiborlem10  36736  heibor  36737  rrndstprj2  36747  cmpidelt  36775  rngoid  36818  fsuppind  41210  limsuc2  41831  cvgdvgrat  43120  cncmpmax  43764  foelrnf  43932  mccllem  44361  mccl  44362  climinf  44370  climsuse  44372  islptre  44383  limcperiod  44392  addlimc  44412  0ellimcdiv  44413  cncficcgt0  44652  dvbdfbdioolem2  44693  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  dvnprodlem3  44712  stoweidlem7  44771  stoweidlem15  44779  stoweidlem21  44785  stoweidlem31  44795  stoweidlem35  44799  stoweidlem36  44800  stoweidlem50  44814  stoweidlem57  44821  stoweidlem59  44823  wallispilem3  44831  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem32  44903  fourierdlem33  44904  fourierdlem39  44910  fourierdlem62  44932  fourierdlem71  44941  fourierdlem89  44959  fourierdlem91  44961  fourierdlem93  44963  fourierdlem101  44971  fourierdlem103  44973  fourierdlem104  44974  etransclem24  45022  etransclem32  45030  smflimlem6  45540  smfpimcc  45572  smfsuplem2  45576  isomushgr  46542