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

Definition df-rel 4484
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4925 and dfrel3 4932. (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 4482 . 2  wff  Rel  A
3 cvv 2641 . . . 4  class  _V
43, 3cxp 4475 . . 3  class  ( _V 
X.  _V )
51, 4wss 3021 . 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  4515  0nelrel  4523  releq  4559  nfrel  4562  sbcrel  4563  relss  4564  ssrel  4565  elrel  4579  relsng  4580  relsn  4582  relxp  4586  relun  4594  reliun  4598  reliin  4599  rel0  4602  relopabi  4603  relop  4627  eqbrrdva  4647  elreldm  4703  issref  4857  cnvcnv  4927  relrelss  5001  cnviinm  5016  nfunv  5092  funinsn  5108  oprabss  5789  1st2nd  6009  1stdm  6010  releldm2  6013  reldmtpos  6080  dmtpos  6083  dftpos4  6090  tpostpos  6091  iinerm  6431  fundmen  6630  frecuzrdgtcl  10026  frecuzrdgfunlem  10033  reldvg  12521
  Copyright terms: Public domain W3C validator