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

Theorem relres 4815
Description: A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
relres  |-  Rel  ( A  |`  B )

Proof of Theorem relres
StepHypRef Expression
1 df-res 4519 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
2 inss2 3265 . . 3  |-  ( A  i^i  ( B  X.  _V ) )  C_  ( B  X.  _V )
31, 2eqsstri 3097 . 2  |-  ( A  |`  B )  C_  ( B  X.  _V )
4 relxp 4616 . 2  |-  Rel  ( B  X.  _V )
5 relss 4594 . 2  |-  ( ( A  |`  B )  C_  ( B  X.  _V )  ->  ( Rel  ( B  X.  _V )  ->  Rel  ( A  |`  B ) ) )
63, 4, 5mp2 16 1  |-  Rel  ( A  |`  B )
Colors of variables: wff set class
Syntax hints:   _Vcvv 2658    i^i cin 3038    C_ wss 3039    X. cxp 4505    |` cres 4509   Rel wrel 4512
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-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-in 3045  df-ss 3052  df-opab 3958  df-xp 4513  df-rel 4514  df-res 4519
This theorem is referenced by:  elres  4823  resiexg  4832  iss  4833  dfres2  4839  issref  4889  asymref  4892  poirr2  4899  cnvcnvres  4970  resco  5011  ressn  5047  funssres  5133  fnresdisj  5201  fnres  5207  fcnvres  5274  nfunsn  5421  fsnunfv  5587  resfunexgALT  5974  setsresg  11903
  Copyright terms: Public domain W3C validator