Theorem rspccva 3587

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  disjne  4418  n0snor2el  4797  seex  5597  preddowncl  6305  frpoins3g  6319  foelrn  7079  foelrnf  7080  caofid0l  7686  caofid0r  7687  caofid1  7688  caofid2  7689  onnseq  8313  odi  8543  omsmolem  8621  naddssim  8649  fvixp  8875  unblem1  9239  ordiso2  9468  unwdomg  9537  ac5num  9989  acni2  9999  fodomacn  10009  iundom2g  10493  fpwwe2lem3  10586  eltsk2g  10704  tskpwss  10705  tskpw  10706  tsken  10707  prlem934  10986  dedekindle  11338  ltord1  11704  leord1  11705  eqord1  11706  ltord2  11707  leord2  11708  eqord2  11709  supmul1  12152  seqcaopr2  14003  bccl  14287  hashbc  14418  limsupbnd2  15449  2clim  15538  climsup  15636  caurcvg2  15644  caucvgb  15646  isummulc2  15728  telfsumo2  15769  fsumparts  15772  incexclem  15802  isumshft  15805  climcndslem1  15815  climcndslem2  15816  supcvg  15822  geomulcvg  15842  mertenslem2  15851  mertens  15852  bpolycl  16018  bpolydif  16021  rpnnen2lem10  16191  dvdsprime  16657  fuciso  17940  lubub  18470  lubl  18471  mgmlrid  18594  grpinvalem  18600  grpinvex  18875  issubg2  19073  issubg4  19077  nmzbi  19096  gagrpid  19226  cntzi  19261  psgnunilem2  19425  sylow1lem3  19530  pgpfi  19535  slwispgp  19541  sylow2alem1  19547  dprdfcl  19945  ablfac2  20021  abveq0  20727  issrngd  20764  phllmhm  21541  ipcl  21542  ipeq0  21547  isphld  21563  ocvi  21578  pf1ind  22242  cayhamlem3  22774  elcls3  22970  neindisj2  23010  perfi  23042  cnima  23152  1stcfb  23332  1stcelcls  23348  llyi  23361  nllyi  23362  locfinnei  23410  1stckgenlem  23440  ptbasin  23464  txcls  23491  ptcnp  23509  ufli  23801  tgpt0  24006  tsmsxplem2  24041  nrmmetd  24462  tngngp  24542  tngngp3  24544  reperflem  24707  lebnumlem3  24862  htpyi  24873  htpycc  24879  phtpyi  24883  cfili  25168  cmetcvg  25185  caubl  25208  caublcls  25209  bcthlem2  25225  bcthlem3  25226  bcthlem4  25227  ovolicc2lem1  25418  ovolicc2lem5  25422  ovolicc2  25423  voliunlem3  25453  volsuplem  25456  uniioombllem2  25484  mbfima  25531  ismbfd  25540  ismbf3d  25555  mbfmullem  25626  itg2monolem1  25651  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  bddmulibl  25740  bddiblnc  25743  c1liplem1  25901  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumrlimf  25931  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlimge0  25937  dvfsum2  25941  ftc1lem6  25948  ulmcau  26304  ulmdvlem1  26309  ulmdvlem3  26311  mtestbdd  26314  itgulm  26317  radcnvlem1  26322  abelthlem5  26345  abelthlem7  26348  areambl  26868  2lgslem1a  27302  dchrisumlem2  27401  dchrvmasumiflem1  27412  pntpbnd1  27497  ostthlem1  27538  madebday  27811  addscom  27873  precsexlem9  28117  peano5n0s  28212  zs12bday  28343  tglowdim1i  28428  brbtwn2  28832  ax5seglem1  28855  ax5seglem2  28856  ax5seglem9  28864  axcontlem4  28894  axcontlem12  28902  fusgreghash2wsp  30267  grpoidinvlem3  30435  grpoidinv  30437  grpoidinv2  30444  vcidOLD  30493  minvecolem5  30810  hcaucvg  31115  hlimconvi  31120  lnopeq0i  31936  cnlnadjlem5  32000  csmdsymi  32263  difelsiga  34123  eulerpartlemb  34359  ballotlemfc0  34484  ballotlemfcc  34485  ptpconn  35220  cvmsdisj  35257  cvmshmeo  35258  snmlflim  35319  elmrsubrn  35507  mvtinf  35542  sinccvg  35660  fnemeet1  36354  fnemeet2  36355  fnejoin1  36356  fnejoin2  36357  bj-seex  36910  poimirlem27  37641  poimirlem32  37646  mblfinlem1  37651  ovoliunnfl  37656  ex-ovoliunnfl  37657  voliunnfl  37658  volsupnfl  37659  mbfresfi  37660  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anc  37695  upixp  37723  filbcmb  37734  sdclem1  37737  seqpo  37741  incsequz2  37743  mettrifi  37751  caushft  37755  sstotbnd2  37768  heibor1lem  37803  heiborlem3  37807  heiborlem10  37814  heibor  37815  rrndstprj2  37825  cmpidelt  37853  rngoid  37896  fsuppind  42578  limsuc2  43030  cvgdvgrat  44302  cncmpmax  45026  mccllem  45595  mccl  45596  climinf  45604  climsuse  45606  islptre  45617  limcperiod  45626  addlimc  45646  0ellimcdiv  45647  cncficcgt0  45886  dvbdfbdioolem2  45927  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem3  45946  stoweidlem7  46005  stoweidlem15  46013  stoweidlem21  46019  stoweidlem31  46029  stoweidlem35  46033  stoweidlem36  46034  stoweidlem50  46048  stoweidlem57  46055  stoweidlem59  46057  wallispilem3  46065  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem32  46137  fourierdlem33  46138  fourierdlem39  46144  fourierdlem62  46166  fourierdlem71  46175  fourierdlem89  46193  fourierdlem91  46195  fourierdlem93  46197  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  etransclem24  46256  etransclem32  46264  smflimlem6  46774  smfpimcc  46806  smfsuplem2  46810  gricushgr  47917