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

Definition df-rel 4267
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4686 and dfrel3 4693. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-rel (Rel AA ⊆ (V × V))

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3 class A
21wrel 4265 . 2 wff Rel A
3 cvv 2526 . . . 4 class V
43, 3cxp 4258 . . 3 class (V × V)
51, 4wss 2885 . 2 wff A ⊆ (V × V)
62, 5wb 98 1 wff (Rel AA ⊆ (V × V))
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4296  releq  4337  nfrel  4340  sbcrel  4341  relss  4342  ssrel  4343  elrel  4357  relsn  4358  relxp  4362  relun  4369  reliun  4373  reliin  4374  rel0  4377  relopabi  4378  relop  4401  eqbrrdva  4420  elreldm  4475  issref  4622  cnvcnv  4688  relrelss  4759  cnviinm  4774  nfunv  4847  oprabss  5501  1st2nd  5718  1stdm  5719  releldm2  5722  reldmtpos  5778  dmtpos  5781  dftpos4  5788  tpostpos  5789  iinerm  6077
  Copyright terms: Public domain W3C validator