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

Definition df-rel 4844
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5280 and dfrel3 5287. (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 4842 . 2  wff  Rel  A
3 cvv 2916 . . . 4  class  _V
43, 3cxp 4835 . . 3  class  ( _V 
X.  _V )
51, 4wss 3280 . 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  4874  releq  4918  nfrel  4921  relss  4922  ssrel  4923  elrel  4937  relsn  4938  relxp  4942  relun  4950  reliun  4954  reliin  4955  rel0  4958  relopabi  4959  relop  4982  eqbrrdva  5001  elreldm  5053  issref  5206  cnvcnv  5282  relrelss  5352  cnviin  5368  nfunv  5443  dff3  5841  oprabss  6118  relmptopab  6251  1st2nd  6352  1stdm  6353  releldm2  6356  exopxfr2  6370  relmpt2opab  6388  reldmtpos  6446  dmtpos  6450  dftpos4  6457  tpostpos  6458  iiner  6935  fundmen  7139  nqerf  8763  uzrdgfni  11253  hashfun  11655  homarel  14146  relxpchom  14233  ustrel  18194  utop2nei  18233  utop3cls  18234  metustrelOLD  18538  metustrel  18539  pi1xfrcnv  19035  reldv  19710  dvbsss  19742  rngosn3  21967  vcoprnelem  22010  vcex  22012  metideq  24241  metider  24242  pstmfval  24244  txprel  25633  relsset  25642  elfuns  25668  fnsingle  25672  funimage  25681  linedegen  25981  mblfinlem  26143  opelopab3  26308  sbcrel  27848  relopabVD  28722  dihvalrel  31762
  Copyright terms: Public domain W3C validator