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

Definition df-rel 4698
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5126 and dfrel3 5133. (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 4696 . 2  wff  Rel  A
3 cvv 2790 . . . 4  class  _V
43, 3cxp 4689 . . 3  class  ( _V 
X.  _V )
51, 4wss 3154 . 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  4728  releq  4773  nfrel  4776  relss  4777  ssrel  4778  elrel  4791  relsn  4792  relxp  4796  relun  4804  reliun  4808  reliin  4809  rel0  4812  relopabi  4813  relop  4836  elreldm  4905  issref  5058  cnvcnv  5128  relrelss  5198  cnviin  5214  nfunv  5287  dff3  5675  oprabss  5935  relmptopab  6067  1st2nd  6168  1stdm  6169  releldm2  6172  exopxfr2  6186  relmpt2opab  6203  reldmtpos  6244  dmtpos  6248  dftpos4  6255  tpostpos  6256  iiner  6733  fundmen  6936  nqerf  8556  uzrdgfni  11023  hashfun  11391  homarel  13870  relxpchom  13957  pi1xfrcnv  18557  reldv  19222  dvbsss  19254  rngosn3  21095  vcoprnelem  21136  vcex  21138  txprel  24421  relsset  24430  elfuns  24456  fnsingle  24460  funimage  24469  linedegen  24768  prj1b  25090  prj3  25091  resid2  25108  relded  25751  reldded  25752  relrded  25753  relcat  25772  reldcat  25773  relrcat  25774  opelopab3  26384  sbcrel  27990  relopabVD  28750  dihvalrel  31542
  Copyright terms: Public domain W3C validator