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

Definition df-rel 4275
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4694 and dfrel3 4701. (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 4273 . 2 wff Rel A
3 cvv 2531 . . . 4 class V
43, 3cxp 4266 . . 3 class (V × V)
51, 4wss 2890 . 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  4304  releq  4345  nfrel  4348  sbcrel  4349  relss  4350  ssrel  4351  elrel  4365  relsn  4366  relxp  4370  relun  4377  reliun  4381  reliin  4382  rel0  4385  relopabi  4386  relop  4409  eqbrrdva  4428  elreldm  4483  issref  4630  cnvcnv  4696  relrelss  4767  cnviinm  4782  nfunv  4855  oprabss  5509  1st2nd  5726  1stdm  5727  releldm2  5730  reldmtpos  5786  dmtpos  5789  dftpos4  5796  tpostpos  5797  iinerm  6085
  Copyright terms: Public domain W3C validator