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

Definition df-rel 4712
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5140 and dfrel3 5147. (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 4710 . 2  wff  Rel  A
3 cvv 2801 . . . 4  class  _V
43, 3cxp 4703 . . 3  class  ( _V 
X.  _V )
51, 4wss 3165 . 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  4742  releq  4787  nfrel  4790  relss  4791  ssrel  4792  elrel  4805  relsn  4806  relxp  4810  relun  4818  reliun  4822  reliin  4823  rel0  4826  relopabi  4827  relop  4850  elreldm  4919  issref  5072  cnvcnv  5142  relrelss  5212  cnviin  5228  nfunv  5301  dff3  5689  oprabss  5949  relmptopab  6081  1st2nd  6182  1stdm  6183  releldm2  6186  exopxfr2  6200  relmpt2opab  6217  reldmtpos  6258  dmtpos  6262  dftpos4  6269  tpostpos  6270  iiner  6747  fundmen  6950  nqerf  8570  uzrdgfni  11037  hashfun  11405  homarel  13884  relxpchom  13971  pi1xfrcnv  18571  reldv  19236  dvbsss  19268  rngosn3  21109  vcoprnelem  21150  vcex  21152  txprel  24490  relsset  24499  elfuns  24525  fnsingle  24529  funimage  24538  linedegen  24838  prj1b  25182  prj3  25183  resid2  25200  relded  25843  reldded  25844  relrded  25845  relcat  25864  reldcat  25865  relrcat  25866  opelopab3  26476  sbcrel  28084  relopabVD  28993  dihvalrel  32091
  Copyright terms: Public domain W3C validator