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

Definition df-rel 4695
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5123 and dfrel3 5129. (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 4693 . 2  wff  Rel  A
3 cvv 2789 . . . 4  class  _V
43, 3cxp 4686 . . 3  class  ( _V 
X.  _V )
51, 4wss 3153 . 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  4725  releq  4770  nfrel  4773  relss  4774  ssrel  4775  elrel  4788  relsn  4789  relxp  4793  relun  4801  reliun  4805  reliin  4806  rel0  4809  relopabi  4810  relop  4833  elreldm  4902  issref  5055  cnvcnv  5125  relrelss  5194  cnviin  5210  nfunv  5251  dff3  5635  oprabss  5895  relmptopab  6027  1st2nd  6128  1stdm  6129  releldm2  6132  exopxfr2  6146  relmpt2opab  6163  reldmtpos  6204  dmtpos  6208  dftpos4  6215  tpostpos  6216  iiner  6727  fundmen  6930  nqerf  8550  uzrdgfni  11017  hashfun  11385  homarel  13864  relxpchom  13951  pi1xfrcnv  18551  reldv  19216  dvbsss  19248  rngosn3  21087  vcoprnelem  21128  vcex  21130  txprel  23830  relsset  23839  elfuns  23864  fnsingle  23868  funimage  23877  linedegen  24176  prj1b  24489  prj3  24490  resid2  24507  relded  25151  reldded  25152  relrded  25153  relcat  25172  reldcat  25173  relrcat  25174  opelopab3  25784  sbcrel  27370  relopabVD  27957  dihvalrel  30748
  Copyright terms: Public domain W3C validator