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 5591
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6085 and dfrel3 6094. (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 5589 . 2 wff Rel 𝐴
3 cvv 3429 . . . 4 class V
43, 3cxp 5582 . . 3 class (V × V)
51, 4wss 3886 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 205 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff setvar class
This definition is referenced by:  relxp  5602  pwvrel  5632  brrelex12  5634  0nelrel0  5642  releq  5681  nfrel  5684  sbcrel  5685  relss  5686  ssrel  5687  elrel  5701  rel0  5702  nrelv  5703  relsng  5704  relun  5714  reliun  5719  reliin  5720  relopabiv  5723  relopabi  5725  relopabiALT  5726  exopxfr2  5746  relop  5752  eqbrrdva  5771  elreldm  5837  cnvcnv  6088  relrelss  6169  cnviin  6182  dff3  6968  oprabss  7371  relmptopab  7509  1st2nd  7869  1stdm  7870  releldm2  7873  relmpoopab  7921  reldmtpos  8037  dmtpos  8041  dftpos4  8048  tpostpos  8049  iiner  8565  fundmen  8808  nqerf  10696  uzrdgfni  13688  hashfun  14162  reltrclfv  14738  homarel  17761  relxpchom  17908  ustrel  23373  utop2nei  23412  utop3cls  23413  metustrel  23718  pi1xfrcnv  24230  reldv  25044  dvbsss  25076  ssrelf  30963  1stpreimas  31046  fpwrelmap  31076  gsumhashmul  31324  metideq  31851  metider  31852  pstmfval  31854  esum2d  32069  txprel  34189  relsset  34198  elfuns  34225  fnsingle  34229  funimage  34238  bj-opelrelex  35323  bj-elid5  35348  mblfinlem1  35822  rngosn3  36090  xrnrel  36511  elrelsrel  36613  dihvalrel  39301  cnvcnvintabd  41189  cnvintabd  41192  clcnvlem  41212  rfovcnvf1od  41593  relopabVD  42502  sprsymrelfo  44927
  Copyright terms: Public domain W3C validator