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

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

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3 class 𝐴
21wrel 4649 . 2 wff Rel 𝐴
3 cvv 2752 . . . 4 class V
43, 3cxp 4642 . . 3 class (V × V)
51, 4wss 3144 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 105 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4682  0nelrel  4690  releq  4726  nfrel  4729  sbcrel  4730  relss  4731  ssrel  4732  elrel  4746  relsng  4747  relsn  4749  relxp  4753  relun  4761  reliun  4765  reliin  4766  rel0  4769  relopabi  4770  relop  4795  eqbrrdva  4815  elreldm  4871  issref  5029  cnvcnv  5099  relrelss  5173  cnviinm  5188  nfunv  5268  funinsn  5284  oprabss  5981  1st2nd  6205  1stdm  6206  releldm2  6209  reldmtpos  6277  dmtpos  6280  dftpos4  6287  tpostpos  6288  iinerm  6632  fundmen  6831  frecuzrdgtcl  10442  frecuzrdgfunlem  10449  reldvdsrsrg  13439  reldvg  14600
  Copyright terms: Public domain W3C validator