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

Definition df-rel 4618
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5061 and dfrel3 5068. (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 4616 . 2 wff Rel 𝐴
3 cvv 2730 . . . 4 class V
43, 3cxp 4609 . . 3 class (V × V)
51, 4wss 3121 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 104 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4649  0nelrel  4657  releq  4693  nfrel  4696  sbcrel  4697  relss  4698  ssrel  4699  elrel  4713  relsng  4714  relsn  4716  relxp  4720  relun  4728  reliun  4732  reliin  4733  rel0  4736  relopabi  4737  relop  4761  eqbrrdva  4781  elreldm  4837  issref  4993  cnvcnv  5063  relrelss  5137  cnviinm  5152  nfunv  5231  funinsn  5247  oprabss  5939  1st2nd  6160  1stdm  6161  releldm2  6164  reldmtpos  6232  dmtpos  6235  dftpos4  6242  tpostpos  6243  iinerm  6585  fundmen  6784  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  reldvg  13442
  Copyright terms: Public domain W3C validator