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

Definition df-rel 4871
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5307 and dfrel3 5314. (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 4869 . 2  wff  Rel  A
3 cvv 2943 . . . 4  class  _V
43, 3cxp 4862 . . 3  class  ( _V 
X.  _V )
51, 4wss 3307 . 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  4901  releq  4945  nfrel  4948  relss  4949  ssrel  4950  elrel  4964  relsn  4965  relxp  4969  relun  4977  reliun  4981  reliin  4982  rel0  4985  relopabi  4986  relop  5009  eqbrrdva  5028  elreldm  5080  issref  5233  cnvcnv  5309  relrelss  5379  cnviin  5395  nfunv  5470  dff3  5868  oprabss  6145  relmptopab  6278  1st2nd  6379  1stdm  6380  releldm2  6383  exopxfr2  6397  relmpt2opab  6415  reldmtpos  6473  dmtpos  6477  dftpos4  6484  tpostpos  6485  iiner  6962  fundmen  7166  nqerf  8791  uzrdgfni  11281  hashfun  11683  homarel  14174  relxpchom  14261  ustrel  18224  utop2nei  18263  utop3cls  18264  metustrelOLD  18568  metustrel  18569  pi1xfrcnv  19065  reldv  19740  dvbsss  19772  rngosn3  21997  vcoprnelem  22040  vcex  22042  metideq  24271  metider  24272  pstmfval  24274  txprel  25669  relsset  25678  elfuns  25705  fnsingle  25709  funimage  25718  linedegen  26020  mblfinlem  26185  opelopab3  26350  sbcrel  27890  relopabVD  28765  dihvalrel  31808
  Copyright terms: Public domain W3C validator