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

Definition df-rel 4877
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5313 and dfrel3 5320. (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 4875 . 2  wff  Rel  A
3 cvv 2948 . . . 4  class  _V
43, 3cxp 4868 . . 3  class  ( _V 
X.  _V )
51, 4wss 3312 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 177 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4907  releq  4951  nfrel  4954  relss  4955  ssrel  4956  elrel  4970  relsn  4971  relxp  4975  relun  4983  reliun  4987  reliin  4988  rel0  4991  relopabi  4992  relop  5015  eqbrrdva  5034  elreldm  5086  issref  5239  cnvcnv  5315  relrelss  5385  cnviin  5401  nfunv  5476  dff3  5874  oprabss  6151  relmptopab  6284  1st2nd  6385  1stdm  6386  releldm2  6389  exopxfr2  6403  relmpt2opab  6421  reldmtpos  6479  dmtpos  6483  dftpos4  6490  tpostpos  6491  iiner  6968  fundmen  7172  nqerf  8799  uzrdgfni  11290  hashfun  11692  homarel  14183  relxpchom  14270  ustrel  18233  utop2nei  18272  utop3cls  18273  metustrelOLD  18577  metustrel  18578  pi1xfrcnv  19074  reldv  19749  dvbsss  19781  rngosn3  22006  vcoprnelem  22049  vcex  22051  metideq  24280  metider  24281  pstmfval  24283  txprel  25716  relsset  25725  elfuns  25752  fnsingle  25756  funimage  25765  linedegen  26069  mblfinlem  26234  opelopab3  26399  sbcrel  27938  relopabVD  28940  dihvalrel  32004
  Copyright terms: Public domain W3C validator