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

Definition df-rel 4420
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4849 and dfrel3 4856. (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 4418 . 2  wff  Rel  A
3 cvv 2615 . . . 4  class  _V
43, 3cxp 4411 . . 3  class  ( _V 
X.  _V )
51, 4wss 2988 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 103 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4449  releq  4490  nfrel  4493  sbcrel  4494  relss  4495  ssrel  4496  elrel  4510  relsng  4511  relsn  4513  relxp  4517  relun  4524  reliun  4528  reliin  4529  rel0  4532  relopabi  4533  relop  4556  eqbrrdva  4576  elreldm  4631  issref  4783  cnvcnv  4851  relrelss  4925  cnviinm  4940  nfunv  5014  funinsn  5030  oprabss  5693  1st2nd  5910  1stdm  5911  releldm2  5914  reldmtpos  5974  dmtpos  5977  dftpos4  5984  tpostpos  5985  iinerm  6318  fundmen  6477  frecuzrdgtcl  9750  frecuzrdgfunlem  9757
  Copyright terms: Public domain W3C validator