Theorem rspccva 3622

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143

This theorem is referenced by:  disjne  4404  n0snor2el  4764  seex  5518  preddowncl  6175  foelrn  6872  caofid0l  7437  caofid0r  7438  caofid1  7439  caofid2  7440  onnseq  7981  odi  8205  omsmolem  8280  fvixp  8466  unblem1  8770  ordiso2  8979  unwdomg  9048  ac5num  9462  acni2  9472  fodomacn  9482  iundom2g  9962  fpwwe2lem3  10055  eltsk2g  10173  tskpwss  10174  tskpw  10175  tsken  10176  prlem934  10455  dedekindle  10804  ltord1  11166  leord1  11167  eqord1  11168  ltord2  11169  leord2  11170  eqord2  11171  supmul1  11610  seqcaopr2  13407  bccl  13683  hashbc  13812  limsupbnd2  14840  2clim  14929  climsup  15026  caurcvg2  15034  caucvgb  15036  isummulc2  15117  telfsumo2  15158  fsumparts  15161  incexclem  15191  isumshft  15194  climcndslem1  15204  climcndslem2  15205  supcvg  15211  geomulcvg  15232  mertenslem2  15241  mertens  15242  bpolycl  15406  bpolydif  15409  rpnnen2lem10  15576  dvdsprime  16031  fuciso  17245  lubub  17729  lubl  17730  mgmlrid  17877  grprinvlem  17883  grpinvex  18113  issubg2  18294  issubg4  18298  nmzbi  18316  gagrpid  18424  cntzi  18459  psgnunilem2  18623  sylow1lem3  18725  pgpfi  18730  slwispgp  18736  sylow2alem1  18742  dprdfcl  19135  ablfac2  19211  abveq0  19597  issrngd  19632  psrbagconf1o  20154  pf1ind  20518  phllmhm  20776  ipcl  20777  ipeq0  20782  isphld  20798  ocvi  20813  cayhamlem3  21495  elcls3  21691  neindisj2  21731  perfi  21763  cnima  21873  1stcfb  22053  1stcelcls  22069  llyi  22082  nllyi  22083  locfinnei  22131  1stckgenlem  22161  ptbasin  22185  txcls  22212  ptcnp  22230  ufli  22522  tgpt0  22727  tsmsxplem2  22762  nrmmetd  23184  tngngp  23263  tngngp3  23265  reperflem  23426  lebnumlem3  23567  htpyi  23578  htpycc  23584  phtpyi  23588  cfili  23871  cmetcvg  23888  caubl  23911  caublcls  23912  bcthlem2  23928  bcthlem3  23929  bcthlem4  23930  ovolicc2lem1  24118  ovolicc2lem5  24122  ovolicc2  24123  voliunlem3  24153  volsuplem  24156  uniioombllem2  24184  mbfima  24231  ismbfd  24240  ismbf3d  24255  mbfmullem  24326  itg2monolem1  24351  itg2i1fseqle  24355  itg2i1fseq  24356  itg2i1fseq2  24357  itg2addlem  24359  bddmulibl  24439  c1liplem1  24593  dvfsumle  24618  dvfsumabs  24620  dvfsumrlimf  24622  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlimge0  24627  dvfsum2  24631  ftc1lem6  24638  ulmcau  24983  ulmdvlem1  24988  ulmdvlem3  24990  mtestbdd  24993  itgulm  24996  radcnvlem1  25001  abelthlem5  25023  abelthlem7  25026  areambl  25536  2lgslem1a  25967  dchrisumlem2  26066  dchrvmasumiflem1  26077  pntpbnd1  26162  ostthlem1  26203  tglowdim1i  26287  brbtwn2  26691  ax5seglem1  26714  ax5seglem2  26715  ax5seglem9  26723  axcontlem4  26753  axcontlem12  26761  fusgreghash2wsp  28117  grpoidinvlem3  28283  grpoidinv  28285  grpoidinv2  28292  vcidOLD  28341  minvecolem5  28658  hcaucvg  28963  hlimconvi  28968  lnopeq0i  29784  cnlnadjlem5  29848  csmdsymi  30111  difelsiga  31392  eulerpartlemb  31626  ballotlemfc0  31750  ballotlemfcc  31751  ptpconn  32480  cvmsdisj  32517  cvmshmeo  32518  snmlflim  32579  elmrsubrn  32767  mvtinf  32802  sinccvg  32916  fnemeet1  33714  fnemeet2  33715  fnejoin1  33716  fnejoin2  33717  bj-seex  34244  poimirlem27  34934  poimirlem32  34939  mblfinlem1  34944  ovoliunnfl  34949  ex-ovoliunnfl  34950  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  itg2gt0cn  34962  bddiblnc  34977  ftc1cnnc  34981  ftc1anc  34990  upixp  35019  filbcmb  35030  sdclem1  35033  seqpo  35037  incsequz2  35039  mettrifi  35047  caushft  35051  sstotbnd2  35067  heibor1lem  35102  heiborlem3  35106  heiborlem10  35113  heibor  35114  rrndstprj2  35124  cmpidelt  35152  rngoid  35195  limsuc2  39690  cvgdvgrat  40694  cncmpmax  41338  foelrnf  41496  mccllem  41927  mccl  41928  climinf  41936  climsuse  41938  islptre  41949  limcperiod  41958  addlimc  41978  0ellimcdiv  41979  cncficcgt0  42220  dvbdfbdioolem2  42263  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnprodlem3  42282  stoweidlem7  42341  stoweidlem15  42349  stoweidlem21  42355  stoweidlem31  42365  stoweidlem35  42369  stoweidlem36  42370  stoweidlem50  42384  stoweidlem57  42391  stoweidlem59  42393  wallispilem3  42401  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem32  42473  fourierdlem33  42474  fourierdlem39  42480  fourierdlem62  42502  fourierdlem71  42511  fourierdlem89  42529  fourierdlem91  42531  fourierdlem93  42533  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  etransclem24  42592  etransclem32  42600  smflimlem6  43101  smfpimcc  43131  smfsuplem2  43135  isomushgr  44040