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

Definition df-rel 4378
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4801 and dfrel3 4808. (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 4376 . 2 wff Rel 𝐴
3 cvv 2602 . . . 4 class V
43, 3cxp 4369 . . 3 class (V × V)
51, 4wss 2974 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 103 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4407  releq  4448  nfrel  4451  sbcrel  4452  relss  4453  ssrel  4454  elrel  4468  relsng  4469  relsn  4471  relxp  4475  relun  4482  reliun  4486  reliin  4487  rel0  4490  relopabi  4491  relop  4514  eqbrrdva  4533  elreldm  4588  issref  4737  cnvcnv  4803  relrelss  4874  cnviinm  4889  nfunv  4963  funinsn  4979  oprabss  5621  1st2nd  5838  1stdm  5839  releldm2  5842  reldmtpos  5902  dmtpos  5905  dftpos4  5912  tpostpos  5913  iinerm  6244  fundmen  6353  frecuzrdgtcl  9494  frecuzrdgfunlem  9501
  Copyright terms: Public domain W3C validator