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

Definition df-rel 4676
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5112 and dfrel3 5118. (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 4666 . 2  wff  Rel  A
3 cvv 2763 . . . 4  class  _V
43, 3cxp 4659 . . 3  class  ( _V 
X.  _V )
51, 4wss 3127 . 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  4714  releq  4759  nfrel  4762  relss  4763  ssrel  4764  elrel  4777  relsn  4778  relxp  4782  relun  4790  reliun  4794  reliin  4795  rel0  4798  relopabi  4799  relop  4822  elreldm  4891  issref  5044  cnvcnv  5114  relrelss  5183  cnviin  5199  nfunv  5224  dff3  5607  oprabss  5867  relmptopab  5999  1st2nd  6100  1stdm  6101  releldm2  6104  exopxfr2  6118  relmpt2opab  6135  reldmtpos  6176  dmtpos  6180  dftpos4  6187  tpostpos  6188  iiner  6699  fundmen  6902  nqerf  8522  uzrdgfni  10988  hashfun  11355  homarel  13831  relxpchom  13918  pi1xfrcnv  18518  reldv  19183  dvbsss  19215  rngosn3  21054  vcoprnelem  21095  vcex  21097  txprel  23796  relsset  23805  elfuns  23830  fnsingle  23834  funimage  23843  linedegen  24142  prj1b  24446  prj3  24447  resid2  24464  relded  25108  reldded  25109  relrded  25110  relcat  25129  reldcat  25130  relrcat  25131  opelopab3  25741  relopabVD  27810  dihvalrel  30719
  Copyright terms: Public domain W3C validator