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

Definition df-rel 4295
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4714 and dfrel3 4721. (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 4293 . 2 wff Rel A
3 cvv 2551 . . . 4 class V
43, 3cxp 4286 . . 3 class (V × V)
51, 4wss 2911 . 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  4324  releq  4365  nfrel  4368  sbcrel  4369  relss  4370  ssrel  4371  elrel  4385  relsn  4386  relxp  4390  relun  4397  reliun  4401  reliin  4402  rel0  4405  relopabi  4406  relop  4429  eqbrrdva  4448  elreldm  4503  issref  4650  cnvcnv  4716  relrelss  4787  cnviinm  4802  nfunv  4876  oprabss  5532  1st2nd  5749  1stdm  5750  releldm2  5753  reldmtpos  5809  dmtpos  5812  dftpos4  5819  tpostpos  5820  iinerm  6114  fundmen  6222  frecuzrdgfn  8859
  Copyright terms: Public domain W3C validator