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

Theorem ssralv 3100
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
Assertion
Ref Expression
ssralv (𝐴𝐵 → (∀𝑥𝐵 𝜑 → ∀𝑥𝐴 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv
StepHypRef Expression
1 ssel 3033 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 75 . 2 (𝐴𝐵 → ((𝑥𝐵𝜑) → (𝑥𝐴𝜑)))
32ralimdv2 2455 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑 → ∀𝑥𝐴 𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1445  wral 2370  wss 3013
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-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  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-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-ral 2375  df-in 3019  df-ss 3026
This theorem is referenced by:  iinss1  3764  poss  4149  sess2  4189  trssord  4231  funco  5088  funimaexglem  5131  isores3  5632  isoini2  5636  smores  6095  smores2  6097  tfrlem5  6117  resixp  6530  ac6sfi  6694  peano5nnnn  7524  peano5nni  8523  caucvgre  10545  rexanuz  10552  cau3lem  10678  isumclim3  10982  fsumiun  11036  strsetsid  11692  tgcn  12075  tgcnp  12076  cnss2  12094  cncnp  12097  sslm  12114  metrest  12308  rescncf  12350  nninfsellemeq  12627
  Copyright terms: Public domain W3C validator