Theorem rspccva 3578

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080

This theorem is used by:  disjne  4410  n0snor2el  4790  seex  5613  preddowncl  6341  frpoins3g  6355  foelrn  7115  foelrnf  7116  caofid0l  7733  caofid0r  7734  caofid1  7735  caofid2  7736  onnseq  8363  odi  8598  omsmolem  8677  naddssim  8706  fvixp  8941  unblem1  9295  ordiso2  9519  unwdomg  9588  ac5num  10125  acni2  10135  fodomacn  10145  iundom2g  10634  fpwwe2lem3  10728  eltsk2g  10846  tskpwss  10847  tskpw  10848  tsken  10849  prlem934  11128  dedekindle  11484  ltord1  11852  leord1  11853  eqord1  11854  ltord2  11855  leord2  11856  eqord2  11857  supmul1  12296  seqcaopr2  14191  bccl  14476  hashbc  14608  limsupbnd2  15662  2clim  15751  climsup  15849  caurcvg2  15857  caucvgb  15859  isummulc2  15940  telfsumo2  15982  fsumparts  15985  incexclem  16017  isumshft  16020  climcndslem1  16030  climcndslem2  16031  supcvg  16037  geomulcvg  16057  mertenslem2  16066  mertens  16067  bpolycl  16230  bpolydif  16233  rpnnen2lem10  16403  dvdsprime  16874  fuciso  18165  lubub  18697  lubl  18698  mgmlrid  18859  grpinvalem  18866  grpinvex  19166  issubg2  19364  issubg4  19368  nmzbi  19386  gagrpid  19520  cntzi  19555  psgnunilem2  19721  sylow1lem3  19826  pgpfi  19831  slwispgp  19837  sylow2alem1  19843  dprdfcl  20241  ablfac2  20317  abveq0  21087  issrngd  21124  phllmhm  21950  ipcl  21951  ipeq0  21956  isphld  21972  ocvi  21987  pf1ind  22685  cayhamlem3  23217  elcls3  23413  neindisj2  23453  perfi  23485  cnima  23595  1stcfb  23775  1stcelcls  23792  llyi  23805  nllyi  23806  locfinnei  23854  1stckgenlem  23884  ptbasin  23908  txcls  23935  ptcnp  23953  ufli  24245  tgpt0  24450  tsmsxplem2  24485  nrmmetd  24905  tngngp  24985  tngngp3  24987  reperflem  25150  lebnumlem3  25296  htpyi  25307  htpycc  25313  phtpyi  25317  cfili  25601  cmetcvg  25618  caubl  25641  caublcls  25642  bcthlem2  25658  bcthlem3  25659  bcthlem4  25660  ovolicc2lem1  25850  ovolicc2lem5  25854  ovolicc2  25855  voliunlem3  25885  volsuplem  25888  uniioombllem2  25916  mbfima  25963  ismbfd  25972  ismbf3d  25987  mbfmullem  26058  itg2monolem1  26083  itg2i1fseqle  26087  itg2i1fseq  26088  itg2i1fseq2  26089  itg2addlem  26091  bddmulibl  26171  bddiblnc  26174  c1liplem1  26328  dvfsumle  26353  dvfsumabs  26355  dvfsumrlimf  26357  dvfsumlem1  26358  dvfsumlem2  26359  dvfsumlem3  26360  dvfsumlem4  26361  dvfsumrlimge0  26362  dvfsum2  26366  ftc1lem6  26373  ulmcau  26734  ulmdvlem1  26739  ulmdvlem3  26741  mtestbdd  26744  itgulm  26747  radcnvlem1  26752  abelthlem5  26774  abelthlem7  26777  areambl  27298  2lgslem1a  27730  dchrisumlem2  27829  dchrvmasumiflem1  27840  pntpbnd1  27925  ostthlem1  27966  madebday  28298  addscom  28364  precsexlem9  28613  peano5n0s  28717  bdayfinbndlem1  28865  tglowdim1i  28976  brbtwn2  29495  ax5seglem1  29518  ax5seglem2  29519  ax5seglem9  29527  axcontlem4  29557  axcontlem12  29565  fusgreghash2wsp  30951  grpoidinvlem3  31120  grpoidinv  31122  grpoidinv2  31129  vcidOLD  31178  minvecolem5  31495  hcaucvg  31800  hlimconvi  31805  lnopeq0i  32621  cnlnadjlem5  32685  csmdsymi  32948  difunielsiga  34818  eulerpartlemb  35053  ballotlemfc0  35178  ballotlemfcc  35179  werankwe  35800  werankwe2  35801  elscottrankss  35810  ptpconn  36119  cvmsdisj  36156  cvmshmeo  36157  snmlflim  36218  elmrsubrn  36406  mvtinf  36441  sinccvg  36559  nmulprop  37066  fnemeet1  37281  fnemeet2  37282  fnejoin1  37283  fnejoin2  37284  bj-seex  37961  poimirlem27  38705  poimirlem32  38710  mblfinlem1  38715  ovoliunnfl  38720  ex-ovoliunnfl  38721  voliunnfl  38722  volsupnfl  38723  mbfresfi  38724  itg2gt0cn  38733  ftc1cnnc  38750  ftc1anc  38759  upixp  38803  filbcmb  38814  sdclem1  38817  seqpo  38821  incsequz2  38823  mettrifi  38831  caushft  38835  sstotbnd2  38848  heibor1lem  38883  heiborlem3  38887  heiborlem10  38894  heibor  38895  rrndstprj2  38905  cmpidelt  38933  rngoid  38976  fsuppind  43758  limsuc2  44188  cvgdvgrat  45437  cncmpmax  46188  mccllem  46748  mccl  46749  climinf  46757  climsuse  46759  islptre  46770  limcperiod  46779  addlimc  46797  0ellimcdiv  46798  cncficcgt0  47037  dvbdfbdioolem2  47078  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  dvnprodlem3  47097  stoweidlem7  47156  stoweidlem15  47164  stoweidlem21  47170  stoweidlem31  47180  stoweidlem35  47184  stoweidlem36  47185  stoweidlem50  47199  stoweidlem57  47206  stoweidlem59  47208  wallispilem3  47216  dirkercncflem2  47253  dirkercncflem4  47255  fourierdlem32  47288  fourierdlem33  47289  fourierdlem39  47295  fourierdlem62  47317  fourierdlem71  47326  fourierdlem89  47344  fourierdlem91  47346  fourierdlem93  47348  fourierdlem101  47356  fourierdlem103  47358  fourierdlem104  47359  etransclem24  47407  etransclem32  47415  smflimlem6  47925  smfpimcc  47957  smfsuplem2  47961  gricushgr  49154