MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rel Unicode version

Definition df-rel 4696
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5124 and dfrel3 5131. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-rel  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3  class  A
21wrel 4694 . 2  wff  Rel  A
3 cvv 2788 . . . 4  class  _V
43, 3cxp 4687 . . 3  class  ( _V 
X.  _V )
51, 4wss 3152 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 176 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4726  releq  4771  nfrel  4774  relss  4775  ssrel  4776  elrel  4789  relsn  4790  relxp  4794  relun  4802  reliun  4806  reliin  4807  rel0  4810  relopabi  4811  relop  4834  elreldm  4903  issref  5056  cnvcnv  5126  relrelss  5196  cnviin  5212  nfunv  5285  dff3  5673  oprabss  5933  relmptopab  6065  1st2nd  6166  1stdm  6167  releldm2  6170  exopxfr2  6184  relmpt2opab  6201  reldmtpos  6242  dmtpos  6246  dftpos4  6253  tpostpos  6254  iiner  6731  fundmen  6934  nqerf  8554  uzrdgfni  11021  hashfun  11389  homarel  13868  relxpchom  13955  pi1xfrcnv  18555  reldv  19220  dvbsss  19252  rngosn3  21093  vcoprnelem  21134  vcex  21136  txprel  24419  relsset  24428  elfuns  24454  fnsingle  24458  funimage  24467  linedegen  24766  prj1b  25079  prj3  25080  resid2  25097  relded  25740  reldded  25741  relrded  25742  relcat  25761  reldcat  25762  relrcat  25763  opelopab3  26373  sbcrel  27979  relopabVD  28677  dihvalrel  31469
  Copyright terms: Public domain W3C validator