Theorem rspccva 3589

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086

This theorem is referenced by:  disjne  4421  n0snor2el  4802  seex  5621  preddowncl  6334  frpoins3g  6348  foelrn  7103  foelrnf  7104  caofid0l  7708  caofid0r  7709  caofid1  7710  caofid2  7711  onnseq  8330  odi  8563  omsmolem  8642  naddssim  8671  fvixp  8899  unblem1  9251  ordiso2  9476  unwdomg  9545  ac5num  10019  acni2  10029  fodomacn  10039  iundom2g  10523  fpwwe2lem3  10617  eltsk2g  10735  tskpwss  10736  tskpw  10737  tsken  10738  prlem934  11017  dedekindle  11373  ltord1  11739  leord1  11740  eqord1  11741  ltord2  11742  leord2  11743  eqord2  11744  supmul1  12183  seqcaopr2  14073  bccl  14357  hashbc  14489  limsupbnd2  15533  2clim  15622  climsup  15720  caurcvg2  15728  caucvgb  15730  isummulc2  15812  telfsumo2  15854  fsumparts  15857  incexclem  15889  isumshft  15892  climcndslem1  15902  climcndslem2  15903  supcvg  15909  geomulcvg  15929  mertenslem2  15938  mertens  15939  bpolycl  16105  bpolydif  16108  rpnnen2lem10  16278  dvdsprime  16744  fuciso  18034  lubub  18566  lubl  18567  mgmlrid  18724  grpinvalem  18730  grpinvex  19009  issubg2  19207  issubg4  19211  nmzbi  19229  gagrpid  19363  cntzi  19398  psgnunilem2  19564  sylow1lem3  19669  pgpfi  19674  slwispgp  19680  sylow2alem1  19686  dprdfcl  20084  ablfac2  20160  abveq0  20898  issrngd  20935  phllmhm  21750  ipcl  21751  ipeq0  21756  isphld  21772  ocvi  21787  pf1ind  22483  cayhamlem3  23012  elcls3  23208  neindisj2  23248  perfi  23280  cnima  23390  1stcfb  23570  1stcelcls  23586  llyi  23599  nllyi  23600  locfinnei  23648  1stckgenlem  23678  ptbasin  23702  txcls  23729  ptcnp  23747  ufli  24039  tgpt0  24244  tsmsxplem2  24279  nrmmetd  24699  tngngp  24779  tngngp3  24781  reperflem  24944  lebnumlem3  25090  htpyi  25101  htpycc  25107  phtpyi  25111  cfili  25395  cmetcvg  25412  caubl  25435  caublcls  25436  bcthlem2  25452  bcthlem3  25453  bcthlem4  25454  ovolicc2lem1  25644  ovolicc2lem5  25648  ovolicc2  25649  voliunlem3  25679  volsuplem  25682  uniioombllem2  25710  mbfima  25757  ismbfd  25766  ismbf3d  25781  mbfmullem  25852  itg2monolem1  25877  itg2i1fseqle  25881  itg2i1fseq  25882  itg2i1fseq2  25883  itg2addlem  25885  bddmulibl  25966  bddiblnc  25969  c1liplem1  26123  dvfsumle  26148  dvfsumabs  26150  dvfsumrlimf  26152  dvfsumlem1  26153  dvfsumlem2  26154  dvfsumlem3  26155  dvfsumlem4  26156  dvfsumrlimge0  26157  dvfsum2  26161  ftc1lem6  26168  ulmcau  26523  ulmdvlem1  26528  ulmdvlem3  26530  mtestbdd  26533  itgulm  26536  radcnvlem1  26541  abelthlem5  26563  abelthlem7  26566  areambl  27088  2lgslem1a  27520  dchrisumlem2  27619  dchrvmasumiflem1  27630  pntpbnd1  27715  ostthlem1  27756  madebday  28058  addscom  28124  precsexlem9  28373  peano5n0s  28477  bdayfinbndlem1  28625  tglowdim1i  28735  brbtwn2  29195  ax5seglem1  29218  ax5seglem2  29219  ax5seglem9  29227  axcontlem4  29257  axcontlem12  29265  fusgreghash2wsp  30629  grpoidinvlem3  30798  grpoidinv  30800  grpoidinv2  30807  vcidOLD  30856  minvecolem5  31173  hcaucvg  31478  hlimconvi  31483  lnopeq0i  32299  cnlnadjlem5  32363  csmdsymi  32626  difelsiga  34467  eulerpartlemb  34702  ballotlemfc0  34827  ballotlemfcc  34828  ptpconn  35623  cvmsdisj  35660  cvmshmeo  35661  snmlflim  35722  elmrsubrn  35910  mvtinf  35945  sinccvg  36063  nmulprop  36580  fnemeet1  36765  fnemeet2  36766  fnejoin1  36767  fnejoin2  36768  bj-seex  37445  poimirlem27  38185  poimirlem32  38190  mblfinlem1  38195  ovoliunnfl  38200  ex-ovoliunnfl  38201  voliunnfl  38202  volsupnfl  38203  mbfresfi  38204  itg2gt0cn  38213  ftc1cnnc  38230  ftc1anc  38239  upixp  38267  filbcmb  38278  sdclem1  38281  seqpo  38285  incsequz2  38287  mettrifi  38295  caushft  38299  sstotbnd2  38312  heibor1lem  38347  heiborlem3  38351  heiborlem10  38358  heibor  38359  rrndstprj2  38369  cmpidelt  38397  rngoid  38440  fsuppind  43213  limsuc2  43659  cvgdvgrat  44914  cncmpmax  45643  mccllem  46204  mccl  46205  climinf  46213  climsuse  46215  islptre  46226  limcperiod  46235  addlimc  46253  0ellimcdiv  46254  cncficcgt0  46493  dvbdfbdioolem2  46534  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnprodlem3  46553  stoweidlem7  46612  stoweidlem15  46620  stoweidlem21  46626  stoweidlem31  46636  stoweidlem35  46640  stoweidlem36  46641  stoweidlem50  46655  stoweidlem57  46662  stoweidlem59  46664  wallispilem3  46672  dirkercncflem2  46709  dirkercncflem4  46711  fourierdlem32  46744  fourierdlem33  46745  fourierdlem39  46751  fourierdlem62  46773  fourierdlem71  46782  fourierdlem89  46800  fourierdlem91  46802  fourierdlem93  46804  fourierdlem101  46812  fourierdlem103  46814  fourierdlem104  46815  etransclem24  46863  etransclem32  46871  smflimlem6  47381  smfpimcc  47413  smfsuplem2  47417  gricushgr  48570