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

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

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3
21wrel 4867 . 2
3 cvv 3015 . . . 4
43, 3cxp 4860 . . 3
51, 4wss 3365 . 2
62, 5wb 178 1
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4898  releq  4944  nfrel  4947  sbcrel  4948  relss  4949  ssrel  4950  elrel  4964  relsn  4965  relxp  4969  relun  4978  reliun  4982  reliin  4983  rel0  4986  relopabi  4987  exopxfr2  5006  relop  5012  eqbrrdva  5031  elreldm  5086  issref  5234  cnvcnv  5310  relrelss  5381  cnviin  5394  nfunv  5469  dff3  5872  oprabss  6188  relmptopab  6318  1st2nd  6626  1stdm  6627  releldm2  6630  relmpt2opab  6661  reldmtpos  6719  dmtpos  6723  dftpos4  6730  tpostpos  6731  iiner  7138  fundmen  7345  nqerf  8978  uzrdgfni  11630  hashfun  12046  homarel  14745  relxpchom  14832  ustrel  19256  utop2nei  19295  utop3cls  19296  metustrelOLD  19600  metustrel  19601  pi1xfrcnv  20097  reldv  20772  dvbsss  20804  rngosn3  23035  vcoprnelem  23078  vcex  23080  ssrelf  25072  fpwrelmap  25163  metideq  25499  metider  25500  pstmfval  25502  txprel  27063  relsset  27072  elfuns  27099  fnsingle  27103  funimage  27112  linedegen  27416  mblfinlem1  27608  opelopab3  27790  relopabVD  30483  dihvalrel  33627
  Copyright terms: Public domain W3C validator