Theorem rspccva 3575

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  disjne  4408  n0snor2el  4793  seex  5614  preddowncl  6330  frpoins3g  6344  foelrn  7101  foelrnf  7102  caofid0l  7712  caofid0r  7713  caofid1  7714  caofid2  7715  onnseq  8334  odi  8567  omsmolem  8646  naddssim  8675  fvixp  8910  unblem1  9263  ordiso2  9488  unwdomg  9557  ac5num  10040  acni2  10050  fodomacn  10060  iundom2g  10549  fpwwe2lem3  10643  eltsk2g  10761  tskpwss  10762  tskpw  10763  tsken  10764  prlem934  11043  dedekindle  11399  ltord1  11765  leord1  11766  eqord1  11767  ltord2  11768  leord2  11769  eqord2  11770  supmul1  12209  seqcaopr2  14103  bccl  14387  hashbc  14519  limsupbnd2  15571  2clim  15660  climsup  15758  caurcvg2  15766  caucvgb  15768  isummulc2  15849  telfsumo2  15891  fsumparts  15894  incexclem  15926  isumshft  15929  climcndslem1  15939  climcndslem2  15940  supcvg  15946  geomulcvg  15966  mertenslem2  15975  mertens  15976  bpolycl  16139  bpolydif  16142  rpnnen2lem10  16312  dvdsprime  16778  fuciso  18068  lubub  18600  lubl  18601  mgmlrid  18761  grpinvalem  18768  grpinvex  19068  issubg2  19266  issubg4  19270  nmzbi  19288  gagrpid  19422  cntzi  19457  psgnunilem2  19623  sylow1lem3  19728  pgpfi  19733  slwispgp  19739  sylow2alem1  19745  dprdfcl  20143  ablfac2  20219  abveq0  20985  issrngd  21022  phllmhm  21846  ipcl  21847  ipeq0  21852  isphld  21868  ocvi  21883  pf1ind  22581  cayhamlem3  23113  elcls3  23309  neindisj2  23349  perfi  23381  cnima  23491  1stcfb  23671  1stcelcls  23688  llyi  23701  nllyi  23702  locfinnei  23750  1stckgenlem  23780  ptbasin  23804  txcls  23831  ptcnp  23849  ufli  24141  tgpt0  24346  tsmsxplem2  24381  nrmmetd  24801  tngngp  24881  tngngp3  24883  reperflem  25046  lebnumlem3  25192  htpyi  25203  htpycc  25209  phtpyi  25213  cfili  25497  cmetcvg  25514  caubl  25537  caublcls  25538  bcthlem2  25554  bcthlem3  25555  bcthlem4  25556  ovolicc2lem1  25746  ovolicc2lem5  25750  ovolicc2  25751  voliunlem3  25781  volsuplem  25784  uniioombllem2  25812  mbfima  25859  ismbfd  25868  ismbf3d  25883  mbfmullem  25954  itg2monolem1  25979  itg2i1fseqle  25983  itg2i1fseq  25984  itg2i1fseq2  25985  itg2addlem  25987  bddmulibl  26067  bddiblnc  26070  c1liplem1  26224  dvfsumle  26249  dvfsumabs  26251  dvfsumrlimf  26253  dvfsumlem1  26254  dvfsumlem2  26255  dvfsumlem3  26256  dvfsumlem4  26257  dvfsumrlimge0  26258  dvfsum2  26262  ftc1lem6  26269  ulmcau  26632  ulmdvlem1  26637  ulmdvlem3  26639  mtestbdd  26642  itgulm  26645  radcnvlem1  26650  abelthlem5  26672  abelthlem7  26675  areambl  27196  2lgslem1a  27628  dchrisumlem2  27727  dchrvmasumiflem1  27738  pntpbnd1  27823  ostthlem1  27864  madebday  28166  addscom  28232  precsexlem9  28481  peano5n0s  28585  bdayfinbndlem1  28733  tglowdim1i  28844  brbtwn2  29363  ax5seglem1  29386  ax5seglem2  29387  ax5seglem9  29395  axcontlem4  29425  axcontlem12  29433  fusgreghash2wsp  30819  grpoidinvlem3  30988  grpoidinv  30990  grpoidinv2  30997  vcidOLD  31046  minvecolem5  31363  hcaucvg  31668  hlimconvi  31673  lnopeq0i  32489  cnlnadjlem5  32553  csmdsymi  32816  difunielsiga  34644  eulerpartlemb  34880  ballotlemfc0  35005  ballotlemfcc  35006  elscottrankss  35631  ptpconn  35813  cvmsdisj  35850  cvmshmeo  35851  snmlflim  35912  elmrsubrn  36100  mvtinf  36135  sinccvg  36253  nmulprop  36771  fnemeet1  36986  fnemeet2  36987  fnejoin1  36988  fnejoin2  36989  bj-seex  37666  poimirlem27  38397  poimirlem32  38402  mblfinlem1  38407  ovoliunnfl  38412  ex-ovoliunnfl  38413  voliunnfl  38414  volsupnfl  38415  mbfresfi  38416  itg2gt0cn  38425  ftc1cnnc  38442  ftc1anc  38451  upixp  38480  filbcmb  38491  sdclem1  38494  seqpo  38498  incsequz2  38500  mettrifi  38508  caushft  38512  sstotbnd2  38525  heibor1lem  38560  heiborlem3  38564  heiborlem10  38571  heibor  38572  rrndstprj2  38582  cmpidelt  38610  rngoid  38653  fsuppind  43437  limsuc2  43883  cvgdvgrat  45138  cncmpmax  45867  mccllem  46428  mccl  46429  climinf  46437  climsuse  46439  islptre  46450  limcperiod  46459  addlimc  46477  0ellimcdiv  46478  cncficcgt0  46717  dvbdfbdioolem2  46758  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  dvnprodlem3  46777  stoweidlem7  46836  stoweidlem15  46844  stoweidlem21  46850  stoweidlem31  46860  stoweidlem35  46864  stoweidlem36  46865  stoweidlem50  46879  stoweidlem57  46886  stoweidlem59  46888  wallispilem3  46896  dirkercncflem2  46933  dirkercncflem4  46935  fourierdlem32  46968  fourierdlem33  46969  fourierdlem39  46975  fourierdlem62  46997  fourierdlem71  47006  fourierdlem89  47024  fourierdlem91  47026  fourierdlem93  47028  fourierdlem101  47036  fourierdlem103  47038  fourierdlem104  47039  etransclem24  47087  etransclem32  47095  smflimlem6  47605  smfpimcc  47637  smfsuplem2  47641  gricushgr  48834