MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rel Structured version   Visualization version   GIF version

Definition df-rel 5530
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6017 and dfrel3 6026. (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 5528 . 2 wff Rel 𝐴
3 cvv 3444 . . . 4 class V
43, 3cxp 5521 . . 3 class (V × V)
51, 4wss 3884 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 209 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff setvar class
This definition is referenced by:  relxp  5541  pwvrel  5570  brrelex12  5572  0nelrel0  5580  releq  5619  nfrel  5622  sbcrel  5623  relss  5624  ssrel  5625  elrel  5639  rel0  5640  nrelv  5641  relsng  5642  relun  5652  reliun  5657  reliin  5658  relopabiv  5661  relopabi  5662  relopabiALT  5663  exopxfr2  5683  relop  5689  eqbrrdva  5708  elreldm  5773  cnvcnv  6020  relrelss  6096  cnviin  6109  dff3  6847  oprabss  7243  relmptopab  7379  1st2nd  7724  1stdm  7725  releldm2  7728  relmpoopab  7776  reldmtpos  7887  dmtpos  7891  dftpos4  7898  tpostpos  7899  iiner  8356  fundmen  8570  nqerf  10345  uzrdgfni  13325  hashfun  13798  reltrclfv  14372  homarel  17292  relxpchom  17427  ustrel  22821  utop2nei  22860  utop3cls  22861  metustrel  23163  pi1xfrcnv  23666  reldv  24477  dvbsss  24509  ssrelf  30383  1stpreimas  30469  fpwrelmap  30499  gsumhashmul  30745  metideq  31250  metider  31251  pstmfval  31253  esum2d  31466  txprel  33454  relsset  33463  elfuns  33490  fnsingle  33494  funimage  33503  bj-opelrelex  34560  bj-elid5  34585  mblfinlem1  35093  rngosn3  35361  xrnrel  35784  elrelsrel  35886  dihvalrel  38574  cnvcnvintabd  40293  cnvintabd  40296  clcnvlem  40316  rfovcnvf1od  40698  relopabVD  41600  sprsymrelfo  44007
  Copyright terms: Public domain W3C validator