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 5091
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5552 and dfrel3 5561. (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 5089 . 2 wff Rel 𝐴
3 cvv 3190 . . . 4 class V
43, 3cxp 5082 . . 3 class (V × V)
51, 4wss 3560 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 196 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff setvar class
This definition is referenced by:  brrelex12  5125  0nelrel  5132  releq  5172  nfrel  5175  sbcrel  5176  relss  5177  ssrel  5178  ssrelOLD  5179  elrel  5193  relsn  5194  relxp  5198  relun  5206  reliun  5210  reliin  5211  rel0  5214  relopabi  5215  relopabiALT  5216  exopxfr2  5236  relop  5242  eqbrrdva  5261  elreldm  5320  issref  5478  cnvcnv  5555  cnvcnvOLD  5556  relrelss  5628  cnviin  5641  nfunv  5889  dff3  6338  oprabss  6711  relmptopab  6848  1st2nd  7174  1stdm  7175  releldm2  7178  relmpt2opab  7219  reldmtpos  7320  dmtpos  7324  dftpos4  7331  tpostpos  7332  iiner  7779  fundmen  7990  nqerf  9712  uzrdgfni  12713  hashfun  13180  reltrclfv  13708  homarel  16626  relxpchom  16761  ustrel  21955  utop2nei  21994  utop3cls  21995  metustrel  22297  pi1xfrcnv  22797  reldv  23574  dvbsss  23606  vcex  27321  ssrelf  29309  1stpreimas  29367  fpwrelmap  29392  metideq  29760  metider  29761  pstmfval  29763  esum2d  29978  txprel  31681  relsset  31690  elfuns  31717  fnsingle  31721  funimage  31730  bj-elid  32757  mblfinlem1  33117  rngosn3  33394  dihvalrel  36087  relintabex  37407  cnvcnvintabd  37426  cnvintabd  37429  clcnvlem  37450  rfovcnvf1od  37819  relopabVD  38659  sprsymrelfo  41065
  Copyright terms: Public domain W3C validator