ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rspccva GIF version

Theorem rspccva 2735
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
StepHypRef Expression
1 rspcv.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
21rspcv 2732 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32impcom 124 1 ((∀𝑥𝐵 𝜑𝐴𝐵) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1296  wcel 1445  wral 2370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-v 2635
This theorem is referenced by:  disjne  3355  seex  4186  fconstfvm  5554  grprinvlem  5877  fvixp  6500  ordiso2  6808  eqord1  8058  eqord2  8059  seq3caopr2  10048  bccl  10306  2clim  10860  isummulc2  10985  telfsumo2  11026  fsumparts  11029  isumshft  11049  mertenslem2  11095  mertensabs  11096  dvdsprime  11547  cnima  12087
  Copyright terms: Public domain W3C validator