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

Definition df-rel 4641
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5077 and dfrel3 5083. (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 4631 . 2  wff  Rel  A
3 cvv 2740 . . . 4  class  _V
43, 3cxp 4624 . . 3  class  ( _V 
X.  _V )
51, 4wss 3094 . 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  4679  releq  4724  nfrel  4727  relss  4728  ssrel  4729  elrel  4742  relsn  4743  relxp  4747  relun  4755  reliun  4759  reliin  4760  rel0  4763  relopabi  4764  relop  4787  elreldm  4856  issref  5009  cnvcnv  5079  relrelss  5148  cnviin  5164  nfunv  5189  dff3  5572  oprabss  5832  relmptopab  5964  1st2nd  6065  1stdm  6066  releldm2  6069  exopxfr2  6083  relmpt2opab  6100  reldmtpos  6141  dmtpos  6145  dftpos4  6152  tpostpos  6153  iiner  6664  fundmen  6867  nqerf  8487  uzrdgfni  10952  hashfun  11319  homarel  13795  relxpchom  13882  pi1xfrcnv  18482  reldv  19147  dvbsss  19179  rngosn3  21018  vcoprnelem  21059  vcex  21061  txprel  23760  relsset  23769  elfuns  23794  fnsingle  23798  funimage  23807  linedegen  24106  prj1b  24410  prj3  24411  resid2  24428  relded  25072  reldded  25073  relrded  25074  relcat  25093  reldcat  25094  relrcat  25095  opelopab3  25705  relopabVD  27690  dihvalrel  30599
  Copyright terms: Public domain W3C validator