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 5556
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6040 and dfrel3 6049. (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 5554 . 2 wff Rel 𝐴
3 cvv 3495 . . . 4 class V
43, 3cxp 5547 . . 3 class (V × V)
51, 4wss 3935 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 207 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff setvar class
This definition is referenced by:  relxp  5567  pwvrel  5596  brrelex12  5598  0nelrel0  5606  releq  5645  nfrel  5648  sbcrel  5649  relss  5650  ssrel  5651  elrel  5665  rel0  5666  nrelv  5667  relsng  5668  relun  5678  reliun  5683  reliin  5684  relopabiv  5687  relopabi  5688  relopabiALT  5689  exopxfr2  5709  relop  5715  eqbrrdva  5734  elreldm  5799  cnvcnv  6043  relrelss  6118  cnviin  6131  dff3  6859  oprabss  7249  relmptopab  7384  1st2nd  7729  1stdm  7730  releldm2  7733  relmpoopab  7780  reldmtpos  7891  dmtpos  7895  dftpos4  7902  tpostpos  7903  iiner  8359  fundmen  8572  nqerf  10341  uzrdgfni  13316  hashfun  13788  reltrclfv  14367  homarel  17286  relxpchom  17421  ustrel  22749  utop2nei  22788  utop3cls  22789  metustrel  23091  pi1xfrcnv  23590  reldv  24397  dvbsss  24429  ssrelf  30295  1stpreimas  30368  fpwrelmap  30396  metideq  31033  metider  31034  pstmfval  31036  esum2d  31252  txprel  33238  relsset  33247  elfuns  33274  fnsingle  33278  funimage  33287  bj-opelrelex  34329  bj-elid5  34354  mblfinlem1  34811  rngosn3  35085  xrnrel  35507  elrelsrel  35609  dihvalrel  38297  cnvcnvintabd  39840  cnvintabd  39843  clcnvlem  39863  rfovcnvf1od  40230  relopabVD  41115  sprsymrelfo  43506
  Copyright terms: Public domain W3C validator