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

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

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3
21wrel 5009 . 2
3 cvv 3109 . . . 4
43, 3cxp 5002 . . 3
51, 4wss 3475 . 2
62, 5wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  brrelex12  5042  releq  5090  nfrel  5093  sbcrel  5094  relss  5095  ssrel  5096  elrel  5110  relsn  5111  relxp  5115  relun  5124  reliun  5128  reliin  5129  rel0  5132  relopabi  5133  exopxfr2  5152  relop  5158  eqbrrdva  5177  elreldm  5232  issref  5385  cnvcnv  5464  relrelss  5536  cnviin  5549  nfunv  5624  dff3  6044  oprabss  6388  relmptopab  6523  1st2nd  6846  1stdm  6847  releldm2  6850  relmpt2opab  6882  reldmtpos  6982  dmtpos  6986  dftpos4  6993  tpostpos  6994  iiner  7402  fundmen  7609  nqerf  9329  uzrdgfni  12069  hashfun  12495  homarel  15363  relxpchom  15450  ustrel  20714  utop2nei  20753  utop3cls  20754  metustrelOLD  21058  metustrel  21059  pi1xfrcnv  21557  reldv  22274  dvbsss  22306  uhgraopelvv  24297  rngosn3  25428  vcoprnelem  25471  vcex  25473  ssrelf  27466  fpwrelmap  27556  metideq  27872  metider  27873  pstmfval  27875  txprel  29529  relsset  29538  elfuns  29565  fnsingle  29569  funimage  29578  mblfinlem1  30051  relopabVD  33701  bj-elid  34599  dihvalrel  37006
  Copyright terms: Public domain W3C validator