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

Definition df-rel 4352
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4771 and dfrel3 4778. (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 4350 . 2  wff  Rel  A
3 cvv 2557 . . . 4  class  _V
43, 3cxp 4343 . . 3  class  ( _V 
X.  _V )
51, 4wss 2917 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 98 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4381  releq  4422  nfrel  4425  sbcrel  4426  relss  4427  ssrel  4428  elrel  4442  relsn  4443  relxp  4447  relun  4454  reliun  4458  reliin  4459  rel0  4462  relopabi  4463  relop  4486  eqbrrdva  4505  elreldm  4560  issref  4707  cnvcnv  4773  relrelss  4844  cnviinm  4859  nfunv  4933  oprabss  5590  1st2nd  5807  1stdm  5808  releldm2  5811  reldmtpos  5868  dmtpos  5871  dftpos4  5878  tpostpos  5879  iinerm  6178  fundmen  6286  frecuzrdgfn  9198
  Copyright terms: Public domain W3C validator