Theorem rspccva 3577

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  disjne  4409  n0snor2el  4791  seex  5591  preddowncl  6298  frpoins3g  6312  foelrn  7061  foelrnf  7062  caofid0l  7665  caofid0r  7666  caofid1  7667  caofid2  7668  onnseq  8286  odi  8516  omsmolem  8595  naddssim  8623  fvixp  8852  unblem1  9204  ordiso2  9432  unwdomg  9501  ac5num  9958  acni2  9968  fodomacn  9978  iundom2g  10462  fpwwe2lem3  10556  eltsk2g  10674  tskpwss  10675  tskpw  10676  tsken  10677  prlem934  10956  dedekindle  11309  ltord1  11675  leord1  11676  eqord1  11677  ltord2  11678  leord2  11679  eqord2  11680  supmul1  12123  seqcaopr2  13973  bccl  14257  hashbc  14388  limsupbnd2  15418  2clim  15507  climsup  15605  caurcvg2  15613  caucvgb  15615  isummulc2  15697  telfsumo2  15738  fsumparts  15741  incexclem  15771  isumshft  15774  climcndslem1  15784  climcndslem2  15785  supcvg  15791  geomulcvg  15811  mertenslem2  15820  mertens  15821  bpolycl  15987  bpolydif  15990  rpnnen2lem10  16160  dvdsprime  16626  fuciso  17914  lubub  18446  lubl  18447  mgmlrid  18604  grpinvalem  18610  grpinvex  18885  issubg2  19083  issubg4  19087  nmzbi  19105  gagrpid  19235  cntzi  19270  psgnunilem2  19436  sylow1lem3  19541  pgpfi  19546  slwispgp  19552  sylow2alem1  19558  dprdfcl  19956  ablfac2  20032  abveq0  20763  issrngd  20800  phllmhm  21599  ipcl  21600  ipeq0  21605  isphld  21621  ocvi  21636  pf1ind  22311  cayhamlem3  22843  elcls3  23039  neindisj2  23079  perfi  23111  cnima  23221  1stcfb  23401  1stcelcls  23417  llyi  23430  nllyi  23431  locfinnei  23479  1stckgenlem  23509  ptbasin  23533  txcls  23560  ptcnp  23578  ufli  23870  tgpt0  24075  tsmsxplem2  24110  nrmmetd  24530  tngngp  24610  tngngp3  24612  reperflem  24775  lebnumlem3  24930  htpyi  24941  htpycc  24947  phtpyi  24951  cfili  25236  cmetcvg  25253  caubl  25276  caublcls  25277  bcthlem2  25293  bcthlem3  25294  bcthlem4  25295  ovolicc2lem1  25486  ovolicc2lem5  25490  ovolicc2  25491  voliunlem3  25521  volsuplem  25524  uniioombllem2  25552  mbfima  25599  ismbfd  25608  ismbf3d  25623  mbfmullem  25694  itg2monolem1  25719  itg2i1fseqle  25723  itg2i1fseq  25724  itg2i1fseq2  25725  itg2addlem  25727  bddmulibl  25808  bddiblnc  25811  c1liplem1  25969  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumrlimf  25999  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsumrlimge0  26005  dvfsum2  26009  ftc1lem6  26016  ulmcau  26372  ulmdvlem1  26377  ulmdvlem3  26379  mtestbdd  26382  itgulm  26385  radcnvlem1  26390  abelthlem5  26413  abelthlem7  26416  areambl  26936  2lgslem1a  27370  dchrisumlem2  27469  dchrvmasumiflem1  27480  pntpbnd1  27565  ostthlem1  27606  madebday  27908  addscom  27974  precsexlem9  28223  peano5n0s  28327  bdayfinbndlem1  28475  tglowdim1i  28585  brbtwn2  28990  ax5seglem1  29013  ax5seglem2  29014  ax5seglem9  29022  axcontlem4  29052  axcontlem12  29060  fusgreghash2wsp  30425  grpoidinvlem3  30594  grpoidinv  30596  grpoidinv2  30603  vcidOLD  30652  minvecolem5  30969  hcaucvg  31274  hlimconvi  31279  lnopeq0i  32095  cnlnadjlem5  32159  csmdsymi  32422  difelsiga  34311  eulerpartlemb  34546  ballotlemfc0  34671  ballotlemfcc  34672  ptpconn  35449  cvmsdisj  35486  cvmshmeo  35487  snmlflim  35548  elmrsubrn  35736  mvtinf  35771  sinccvg  35889  fnemeet1  36582  fnemeet2  36583  fnejoin1  36584  fnejoin2  36585  bj-seex  37170  poimirlem27  37898  poimirlem32  37903  mblfinlem1  37908  ovoliunnfl  37913  ex-ovoliunnfl  37914  voliunnfl  37915  volsupnfl  37916  mbfresfi  37917  itg2gt0cn  37926  ftc1cnnc  37943  ftc1anc  37952  upixp  37980  filbcmb  37991  sdclem1  37994  seqpo  37998  incsequz2  38000  mettrifi  38008  caushft  38012  sstotbnd2  38025  heibor1lem  38060  heiborlem3  38064  heiborlem10  38071  heibor  38072  rrndstprj2  38082  cmpidelt  38110  rngoid  38153  fsuppind  42948  limsuc2  43398  cvgdvgrat  44669  cncmpmax  45392  mccllem  45957  mccl  45958  climinf  45966  climsuse  45968  islptre  45979  limcperiod  45988  addlimc  46006  0ellimcdiv  46007  cncficcgt0  46246  dvbdfbdioolem2  46287  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnprodlem3  46306  stoweidlem7  46365  stoweidlem15  46373  stoweidlem21  46379  stoweidlem31  46389  stoweidlem35  46393  stoweidlem36  46394  stoweidlem50  46408  stoweidlem57  46415  stoweidlem59  46417  wallispilem3  46425  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem32  46497  fourierdlem33  46498  fourierdlem39  46504  fourierdlem62  46526  fourierdlem71  46535  fourierdlem89  46553  fourierdlem91  46555  fourierdlem93  46557  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  etransclem24  46616  etransclem32  46624  smflimlem6  47134  smfpimcc  47166  smfsuplem2  47170  gricushgr  48277