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

Definition df-rel 4408
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4835 and dfrel3 4842. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-rel  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3  class  A
21wrel 4406 . 2  wff  Rel  A
3 cvv 2612 . . . 4  class  _V
43, 3cxp 4399 . . 3  class  ( _V 
X.  _V )
51, 4wss 2984 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 103 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4437  releq  4478  nfrel  4481  sbcrel  4482  relss  4483  ssrel  4484  elrel  4498  relsng  4499  relsn  4501  relxp  4505  relun  4512  reliun  4516  reliin  4517  rel0  4520  relopabi  4521  relop  4544  eqbrrdva  4564  elreldm  4619  issref  4769  cnvcnv  4837  relrelss  4911  cnviinm  4926  nfunv  5000  funinsn  5016  oprabss  5669  1st2nd  5886  1stdm  5887  releldm2  5890  reldmtpos  5950  dmtpos  5953  dftpos4  5960  tpostpos  5961  iinerm  6294  fundmen  6453  frecuzrdgtcl  9708  frecuzrdgfunlem  9715
  Copyright terms: Public domain W3C validator