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

Definition df-rel 4516
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4959 and dfrel3 4966. (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 4514 . 2  wff  Rel  A
3 cvv 2660 . . . 4  class  _V
43, 3cxp 4507 . . 3  class  ( _V 
X.  _V )
51, 4wss 3041 . 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  4547  0nelrel  4555  releq  4591  nfrel  4594  sbcrel  4595  relss  4596  ssrel  4597  elrel  4611  relsng  4612  relsn  4614  relxp  4618  relun  4626  reliun  4630  reliin  4631  rel0  4634  relopabi  4635  relop  4659  eqbrrdva  4679  elreldm  4735  issref  4891  cnvcnv  4961  relrelss  5035  cnviinm  5050  nfunv  5126  funinsn  5142  oprabss  5825  1st2nd  6047  1stdm  6048  releldm2  6051  reldmtpos  6118  dmtpos  6121  dftpos4  6128  tpostpos  6129  iinerm  6469  fundmen  6668  frecuzrdgtcl  10140  frecuzrdgfunlem  10147  reldvg  12728
  Copyright terms: Public domain W3C validator