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

Definition df-rel 4379
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4798 and dfrel3 4805. (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 4377 . 2  wff  Rel  A
3 cvv 2574 . . . 4  class  _V
43, 3cxp 4370 . . 3  class  ( _V 
X.  _V )
51, 4wss 2944 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 102 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4408  releq  4449  nfrel  4452  sbcrel  4453  relss  4454  ssrel  4455  elrel  4469  relsn  4470  relxp  4474  relun  4481  reliun  4485  reliin  4486  rel0  4489  relopabi  4490  relop  4513  eqbrrdva  4532  elreldm  4587  issref  4734  cnvcnv  4800  relrelss  4871  cnviinm  4886  nfunv  4960  oprabss  5617  1st2nd  5834  1stdm  5835  releldm2  5838  reldmtpos  5898  dmtpos  5901  dftpos4  5908  tpostpos  5909  iinerm  6208  fundmen  6316  frecuzrdgfn  9361
  Copyright terms: Public domain W3C validator