Theorem rspccva 3612

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063

This theorem is referenced by:  disjne  4455  n0snor2el  4835  seex  5639  preddowncl  6334  frpoins3g  6348  foelrn  7108  caofid0l  7701  caofid0r  7702  caofid1  7703  caofid2  7704  onnseq  8344  odi  8579  omsmolem  8656  naddssim  8684  fvixp  8896  unblem1  9295  ordiso2  9510  unwdomg  9579  ac5num  10031  acni2  10041  fodomacn  10051  iundom2g  10535  fpwwe2lem3  10628  eltsk2g  10746  tskpwss  10747  tskpw  10748  tsken  10749  prlem934  11028  dedekindle  11378  ltord1  11740  leord1  11741  eqord1  11742  ltord2  11743  leord2  11744  eqord2  11745  supmul1  12183  seqcaopr2  14004  bccl  14282  hashbc  14412  limsupbnd2  15427  2clim  15516  climsup  15616  caurcvg2  15624  caucvgb  15626  isummulc2  15708  telfsumo2  15749  fsumparts  15752  incexclem  15782  isumshft  15785  climcndslem1  15795  climcndslem2  15796  supcvg  15802  geomulcvg  15822  mertenslem2  15831  mertens  15832  bpolycl  15996  bpolydif  15999  rpnnen2lem10  16166  dvdsprime  16624  fuciso  17928  lubub  18464  lubl  18465  mgmlrid  18586  grprinvlem  18592  grpinvex  18829  issubg2  19021  issubg4  19025  nmzbi  19044  gagrpid  19158  cntzi  19193  psgnunilem2  19363  sylow1lem3  19468  pgpfi  19473  slwispgp  19479  sylow2alem1  19485  dprdfcl  19883  ablfac2  19959  abveq0  20434  issrngd  20469  phllmhm  21185  ipcl  21186  ipeq0  21191  isphld  21207  ocvi  21222  psrbagconf1oOLD  21490  pf1ind  21874  cayhamlem3  22389  elcls3  22587  neindisj2  22627  perfi  22659  cnima  22769  1stcfb  22949  1stcelcls  22965  llyi  22978  nllyi  22979  locfinnei  23027  1stckgenlem  23057  ptbasin  23081  txcls  23108  ptcnp  23126  ufli  23418  tgpt0  23623  tsmsxplem2  23658  nrmmetd  24083  tngngp  24171  tngngp3  24173  reperflem  24334  lebnumlem3  24479  htpyi  24490  htpycc  24496  phtpyi  24500  cfili  24785  cmetcvg  24802  caubl  24825  caublcls  24826  bcthlem2  24842  bcthlem3  24843  bcthlem4  24844  ovolicc2lem1  25034  ovolicc2lem5  25038  ovolicc2  25039  voliunlem3  25069  volsuplem  25072  uniioombllem2  25100  mbfima  25147  ismbfd  25156  ismbf3d  25171  mbfmullem  25243  itg2monolem1  25268  itg2i1fseqle  25272  itg2i1fseq  25273  itg2i1fseq2  25274  itg2addlem  25276  bddmulibl  25356  bddiblnc  25359  c1liplem1  25513  dvfsumle  25538  dvfsumabs  25540  dvfsumrlimf  25542  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlimge0  25547  dvfsum2  25551  ftc1lem6  25558  ulmcau  25907  ulmdvlem1  25912  ulmdvlem3  25914  mtestbdd  25917  itgulm  25920  radcnvlem1  25925  abelthlem5  25947  abelthlem7  25950  areambl  26463  2lgslem1a  26894  dchrisumlem2  26993  dchrvmasumiflem1  27004  pntpbnd1  27089  ostthlem1  27130  madebday  27394  addscom  27450  precsexlem9  27661  tglowdim1i  27752  brbtwn2  28163  ax5seglem1  28186  ax5seglem2  28187  ax5seglem9  28195  axcontlem4  28225  axcontlem12  28233  fusgreghash2wsp  29591  grpoidinvlem3  29759  grpoidinv  29761  grpoidinv2  29768  vcidOLD  29817  minvecolem5  30134  hcaucvg  30439  hlimconvi  30444  lnopeq0i  31260  cnlnadjlem5  31324  csmdsymi  31587  difelsiga  33131  eulerpartlemb  33367  ballotlemfc0  33491  ballotlemfcc  33492  ptpconn  34224  cvmsdisj  34261  cvmshmeo  34262  snmlflim  34323  elmrsubrn  34511  mvtinf  34546  sinccvg  34658  gg-dvfsumle  35182  gg-dvfsumlem2  35183  fnemeet1  35251  fnemeet2  35252  fnejoin1  35253  fnejoin2  35254  bj-seex  35802  poimirlem27  36515  poimirlem32  36520  mblfinlem1  36525  ovoliunnfl  36530  ex-ovoliunnfl  36531  voliunnfl  36532  volsupnfl  36533  mbfresfi  36534  itg2gt0cn  36543  ftc1cnnc  36560  ftc1anc  36569  upixp  36597  filbcmb  36608  sdclem1  36611  seqpo  36615  incsequz2  36617  mettrifi  36625  caushft  36629  sstotbnd2  36642  heibor1lem  36677  heiborlem3  36681  heiborlem10  36688  heibor  36689  rrndstprj2  36699  cmpidelt  36727  rngoid  36770  fsuppind  41162  limsuc2  41783  cvgdvgrat  43072  cncmpmax  43716  foelrnf  43884  mccllem  44313  mccl  44314  climinf  44322  climsuse  44324  islptre  44335  limcperiod  44344  addlimc  44364  0ellimcdiv  44365  cncficcgt0  44604  dvbdfbdioolem2  44645  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem3  44664  stoweidlem7  44723  stoweidlem15  44731  stoweidlem21  44737  stoweidlem31  44747  stoweidlem35  44751  stoweidlem36  44752  stoweidlem50  44766  stoweidlem57  44773  stoweidlem59  44775  wallispilem3  44783  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem32  44855  fourierdlem33  44856  fourierdlem39  44862  fourierdlem62  44884  fourierdlem71  44893  fourierdlem89  44911  fourierdlem91  44913  fourierdlem93  44915  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  etransclem24  44974  etransclem32  44982  smflimlem6  45492  smfpimcc  45524  smfsuplem2  45528  isomushgr  46494