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

Definition df-rel 4514
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4957 and dfrel3 4964. (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 4512 . 2 wff Rel 𝐴
3 cvv 2658 . . . 4 class V
43, 3cxp 4505 . . 3 class (V × V)
51, 4wss 3039 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 104 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4545  0nelrel  4553  releq  4589  nfrel  4592  sbcrel  4593  relss  4594  ssrel  4595  elrel  4609  relsng  4610  relsn  4612  relxp  4616  relun  4624  reliun  4628  reliin  4629  rel0  4632  relopabi  4633  relop  4657  eqbrrdva  4677  elreldm  4733  issref  4889  cnvcnv  4959  relrelss  5033  cnviinm  5048  nfunv  5124  funinsn  5140  oprabss  5823  1st2nd  6045  1stdm  6046  releldm2  6049  reldmtpos  6116  dmtpos  6119  dftpos4  6126  tpostpos  6127  iinerm  6467  fundmen  6666  frecuzrdgtcl  10125  frecuzrdgfunlem  10132  reldvg  12700
  Copyright terms: Public domain W3C validator