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

Theorem ssralv 3202
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
Assertion
Ref Expression
ssralv  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem ssralv
StepHypRef Expression
1 ssel 3132 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 75 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2534 1  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2135   A.wral 2442    C_ wss 3112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-ral 2447  df-in 3118  df-ss 3125
This theorem is referenced by:  iinss1  3873  poss  4271  sess2  4311  trssord  4353  funco  5223  funimaexglem  5266  isores3  5778  isoini2  5782  smores  6252  smores2  6254  tfrlem5  6274  resixp  6691  ac6sfi  6856  difinfinf  7058  peano5nnnn  7825  peano5nni  8852  caucvgre  10913  rexanuz  10920  cau3lem  11046  isumclim3  11354  fsumiun  11408  pcfac  12269  ctinf  12326  strsetsid  12390  tgcn  12775  tgcnp  12776  cnss2  12794  cncnp  12797  sslm  12814  metrest  13073  rescncf  13135  suplociccex  13170  limcresi  13202  nninfsellemeq  13756
  Copyright terms: Public domain W3C validator