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 5265
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5733 and dfrel3 5742. (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 5263 . 2 wff Rel 𝐴
3 cvv 3332 . . . 4 class V
43, 3cxp 5256 . . 3 class (V × V)
51, 4wss 3707 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 196 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff setvar class
This definition is referenced by:  relxp  5275  brrelex12  5304  0nelrel  5311  releq  5350  nfrel  5353  sbcrel  5354  relss  5355  ssrel  5356  ssrelOLD  5357  elrel  5371  relsng  5372  relsnOLD  5375  relun  5383  reliun  5387  reliin  5388  rel0  5391  nrelv  5392  relopabi  5393  relopabiALT  5394  exopxfr2  5414  relop  5420  eqbrrdva  5439  elreldm  5497  issref  5659  cnvcnv  5736  cnvcnvOLD  5737  relrelss  5812  cnviin  5825  nfunv  6074  dff3  6527  oprabss  6903  relmptopab  7040  1st2nd  7373  1stdm  7374  releldm2  7377  relmpt2opab  7419  reldmtpos  7521  dmtpos  7525  dftpos4  7532  tpostpos  7533  iiner  7978  fundmen  8187  nqerf  9936  uzrdgfni  12943  hashfun  13408  reltrclfv  13949  homarel  16879  relxpchom  17014  ustrel  22208  utop2nei  22247  utop3cls  22248  metustrel  22550  pi1xfrcnv  23049  reldv  23825  dvbsss  23857  vcex  27734  ssrelf  29726  1stpreimas  29784  fpwrelmap  29809  metideq  30237  metider  30238  pstmfval  30240  esum2d  30456  txprel  32284  relsset  32293  elfuns  32320  fnsingle  32324  funimage  32333  bj-elid  33388  mblfinlem1  33751  rngosn3  34028  xrnrel  34450  elrelsrel  34552  dihvalrel  37062  relintabex  38381  cnvcnvintabd  38400  cnvintabd  38403  clcnvlem  38424  rfovcnvf1od  38792  relopabVD  39628  sprsymrelfo  42249
  Copyright terms: Public domain W3C validator