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

Definition df-rel 4595
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5031 and dfrel3 5037. (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 4585 . 2  wff  Rel  A
3 cvv 2727 . . . 4  class  _V
43, 3cxp 4578 . . 3  class  ( _V 
X.  _V )
51, 4wss 3078 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 178 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4633  releq  4678  nfrel  4681  relss  4682  ssrel  4683  elrel  4696  relsn  4697  relxp  4701  relun  4709  reliun  4713  reliin  4714  rel0  4717  relopabi  4718  relop  4741  elreldm  4810  issref  4963  cnvcnv  5033  relrelss  5102  cnviin  5118  nfunv  5143  dff3  5525  oprabss  5785  relmptopab  5917  1st2nd  6018  1stdm  6019  releldm2  6022  exopxfr2  6036  relmpt2opab  6053  reldmtpos  6094  dmtpos  6098  dftpos4  6105  tpostpos  6106  iiner  6617  fundmen  6819  nqerf  8434  uzrdgfni  10899  hashfun  11266  homarel  13712  relxpchom  13799  pi1xfrcnv  18387  reldv  19052  dvbsss  19084  rngosn3  20923  vcoprnelem  20964  vcex  20966  txprel  23594  relsset  23603  elfuns  23628  fnsingle  23632  funimage  23641  linedegen  23940  prj1b  24244  prj3  24245  resid2  24262  relded  24906  reldded  24907  relrded  24908  relcat  24927  reldcat  24928  relrcat  24929  opelopab3  25539  relopabVD  27367  dihvalrel  30158
  Copyright terms: Public domain W3C validator