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

Definition df-rel 4553
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4996 and dfrel3 5003. (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 4551 . 2  wff  Rel  A
3 cvv 2689 . . . 4  class  _V
43, 3cxp 4544 . . 3  class  ( _V 
X.  _V )
51, 4wss 3075 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 104 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4584  0nelrel  4592  releq  4628  nfrel  4631  sbcrel  4632  relss  4633  ssrel  4634  elrel  4648  relsng  4649  relsn  4651  relxp  4655  relun  4663  reliun  4667  reliin  4668  rel0  4671  relopabi  4672  relop  4696  eqbrrdva  4716  elreldm  4772  issref  4928  cnvcnv  4998  relrelss  5072  cnviinm  5087  nfunv  5163  funinsn  5179  oprabss  5864  1st2nd  6086  1stdm  6087  releldm2  6090  reldmtpos  6157  dmtpos  6160  dftpos4  6167  tpostpos  6168  iinerm  6508  fundmen  6707  frecuzrdgtcl  10215  frecuzrdgfunlem  10222  reldvg  12854
  Copyright terms: Public domain W3C validator