Theorem rspcva 3578

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcva	⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3576	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 412	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  rexraleqim  3604  fsneq  7065  fvn0ssdmfun  7106  fveqdmss  7110  fvcofneq  7125  wfr3g  8375  boxriin  9006  boxcutc  9007  pwssfi  9230  marypha1lem  9462  supmo  9481  infmo  9526  unwdomg  9615  frr3g  9797  hfelhf  9951  isinffi  10112  axdc3lem2  10568  grothac  10954  nqereu  11053  nnsub  12422  zextle  12812  xrsupsslem  13477  xrinfmsslem  13478  supxrunb1  13489  supxrunb2  13490  injresinjlem  13965  ssnn0fi  14168  suppssfz  14177  faclbnd4lem4  14481  ishashinf  14649  rexuz3  15560  cau3lem  15566  caubnd2  15569  o1co  15797  climcn1  15803  incexclem  16049  dvdsext  16535  mreintcl  17815  initoeu1  18236  initoeu2  18241  termoeu1  18243  lublecllem  18582  mgmidmo  18888  gsumval2  18925  dfgrp3lem  19298  symgfix2  19681  odeq  19815  gexid  19846  ringurd  20462  o2timesd  20487  rglcom4d  20488  gsummoncoe1  22681  m2detleiblem3  22999  m2detleiblem4  23000  cpmatmcllem  23091  mp2pm2mplem4  23182  cayleyhamilton1  23265  cmpsublem  23772  cmpsub  23773  cmpfii  23782  ptpjcn  23985  isufil2  24282  ufileu  24293  lmmbr  25634  caussi  25673  plyco0  26565  dgrco  26649  emcllem7  27386  isppw2  27499  addsrid  28407  mulsrid  28556  n0subs  28806  uvtxnbgrvtx  30031  rusgrnumwwlks  30623  clwwlkf  30695  vdgn1frgrv2  30954  frgrregorufr  30983  grpoidinvlem3  31165  grpoideu  31168  lnconi  32692  fsumiunle  33516  tpr2rico  34655  esumiun  34837  0elsiga  34857  sigaclci  34875  dya2icoseg2  35021  derangsn  36143  sat1el2xp  36352  mirimanofffr  36670  fwddifnp1  37145  poimirlem25  38831  poimirlem26  38832  poimirlem30  38836  poimirlem31  38837  poimirlem32  38838  heicant  38841  mblfinlem2  38844  ftc1anc  38887  fdc  38945  bndss  38986  isdrngo2  39158  divrngidl  39228  maxidlmax  39243  cdleme0nex  41613  dihglblem2N  42617  hgmapvs  43214  ismrcd1  43975  nacsfg  43982  isnacs3  43987  nacsfix  43989  mzpcl1  44006  mzpcl2  44007  mzpcong  44245  dnnumch1  44317  aomclem1  44322  aomclem6  44327  lnr2i  44383  hbtlem5  44395  hbt  44397  rexanuz3  46384  choicefi  46487  suplesup  46624  xralrple2  46639  infxr  46651  infleinf  46656  xralrple4  46657  xralrple3  46658  xrralrecnnge  46674  supxrunb3  46683  supxrleubrnmpt  46689  unb2ltle  46698  suprleubrnmpt  46705  infxrgelbrnmpt  46737  supminfxr  46747  xrpnf  46768  islpcn  46922  limclner  46934  climd  46955  clim2d  46956  limsupmnflem  47003  limsupre3uzlem  47018  xlimpnfxnegmnf  47097  xlimxrre  47114  xlimmnfvlem1  47115  xlimmnfv  47117  xlimpnfvlem1  47119  xlimpnfv  47121  climxlim2lem  47128  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  fourierdlem103  47492  fourierdlem104  47493  etransclem48  47565  saluncl  47600  subsaliuncllem  47640  sge0pnffigt  47679  omessle  47781  caragensplit  47783  omeunile  47788  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvle  47883  vonvolmbllem  47943  vonvolmbl  47944  pimdecfgtioc  47998  smfpreimalt  48014  smfpreimaltf  48019  smfpreimale  48037  smfpreimagt  48045  smfpreimage  48065  smfmullem4  48077  smfinflem  48100  iccpartrn  48785  iccpartiun  48789  icceuelpart  48791  lidldomn1  49601  ply1mulgsumlem2  49830  lindslinindsimp2lem5  49905  lindslinindsimp2  49906  snlindsntor  49914  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0sumshdig  50066