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 5150
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5618 and dfrel3 5627. (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 5148 . 2 wff Rel 𝐴
3 cvv 3231 . . . 4 class V
43, 3cxp 5141 . . 3 class (V × V)
51, 4wss 3607 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 196 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff setvar class
This definition is referenced by:  relxp  5160  brrelex12  5189  0nelrel  5196  releq  5235  nfrel  5238  sbcrel  5239  relss  5240  ssrel  5241  ssrelOLD  5242  elrel  5256  relsng  5257  relsnOLD  5260  relun  5268  reliun  5272  reliin  5273  rel0  5276  nrelv  5277  relopabi  5278  relopabiALT  5279  exopxfr2  5299  relop  5305  eqbrrdva  5324  elreldm  5382  issref  5544  cnvcnv  5621  cnvcnvOLD  5622  relrelss  5697  cnviin  5710  nfunv  5959  dff3  6412  oprabss  6788  relmptopab  6925  1st2nd  7258  1stdm  7259  releldm2  7262  relmpt2opab  7304  reldmtpos  7405  dmtpos  7409  dftpos4  7416  tpostpos  7417  iiner  7862  fundmen  8071  nqerf  9790  uzrdgfni  12797  hashfun  13262  reltrclfv  13802  homarel  16733  relxpchom  16868  ustrel  22062  utop2nei  22101  utop3cls  22102  metustrel  22404  pi1xfrcnv  22903  reldv  23679  dvbsss  23711  vcex  27561  ssrelf  29553  1stpreimas  29611  fpwrelmap  29636  metideq  30064  metider  30065  pstmfval  30067  esum2d  30283  txprel  32111  relsset  32120  elfuns  32147  fnsingle  32151  funimage  32160  bj-elid  33215  mblfinlem1  33576  rngosn3  33853  xrnrel  34275  elrelsrel  34377  dihvalrel  36885  relintabex  38204  cnvcnvintabd  38223  cnvintabd  38226  clcnvlem  38247  rfovcnvf1od  38615  relopabVD  39451  sprsymrelfo  42072
  Copyright terms: Public domain W3C validator