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

Definition df-rel 4926
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5365 and dfrel3 5372. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-rel

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3
21wrel 4924 . 2
3 cvv 2965 . . . 4
43, 3cxp 4917 . . 3
51, 4wss 3309 . 2
62, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4955  releq  5001  nfrel  5004  relss  5005  ssrel  5006  elrel  5020  relsn  5021  relxp  5025  relun  5033  reliun  5037  reliin  5038  rel0  5041  relopabi  5042  relop  5065  eqbrrdva  5084  elreldm  5138  issref  5291  cnvcnv  5367  relrelss  5439  cnviin  5455  nfunv  5531  dff3  5930  oprabss  6209  relmptopab  6342  1st2nd  6443  1stdm  6444  releldm2  6447  exopxfr2  6461  relmpt2opab  6479  reldmtpos  6537  dmtpos  6541  dftpos4  6548  tpostpos  6549  iiner  7025  fundmen  7229  nqerf  8858  uzrdgfni  11349  hashfun  11751  homarel  14242  relxpchom  14329  ustrel  18292  utop2nei  18331  utop3cls  18332  metustrelOLD  18636  metustrel  18637  pi1xfrcnv  19133  reldv  19808  dvbsss  19840  rngosn3  22065  vcoprnelem  22108  vcex  22110  metideq  24337  metider  24338  pstmfval  24340  ssrelf  24732  fpwrelmap  24737  txprel  25828  relsset  25837  elfuns  25864  fnsingle  25868  funimage  25877  linedegen  26181  mblfinlem1  26352  opelopab3  26529  sbcrel  28135  relopabVD  29254  dihvalrel  32317
  Copyright terms: Public domain W3C validator