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

Definition df-rel 4651
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5097 and dfrel3 5104. (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 4649 . 2  wff  Rel  A
3 cvv 2752 . . . 4  class  _V
43, 3cxp 4642 . . 3  class  ( _V 
X.  _V )
51, 4wss 3144 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 105 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4682  0nelrel  4690  releq  4726  nfrel  4729  sbcrel  4730  relss  4731  ssrel  4732  elrel  4746  relsng  4747  relsn  4749  relxp  4753  relun  4761  reliun  4765  reliin  4766  rel0  4769  relopabi  4770  relop  4795  eqbrrdva  4815  elreldm  4871  issref  5029  cnvcnv  5099  relrelss  5173  cnviinm  5188  nfunv  5268  funinsn  5284  oprabss  5982  1st2nd  6206  1stdm  6207  releldm2  6210  reldmtpos  6278  dmtpos  6281  dftpos4  6288  tpostpos  6289  iinerm  6633  fundmen  6832  frecuzrdgtcl  10443  frecuzrdgfunlem  10450  relelbasov  12574  reldvdsrsrg  13442  reldvg  14605
  Copyright terms: Public domain W3C validator