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

Definition df-rel 4778
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5206 and dfrel3 5213. (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 4776 . 2  wff  Rel  A
3 cvv 2864 . . . 4  class  _V
43, 3cxp 4769 . . 3  class  ( _V 
X.  _V )
51, 4wss 3228 . 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  4808  releq  4853  nfrel  4856  relss  4857  ssrel  4858  elrel  4871  relsn  4872  relxp  4876  relun  4884  reliun  4888  reliin  4889  rel0  4892  relopabi  4893  relop  4916  elreldm  4985  issref  5138  cnvcnv  5208  relrelss  5278  cnviin  5294  nfunv  5367  dff3  5756  oprabss  6020  relmptopab  6152  1st2nd  6253  1stdm  6254  releldm2  6257  exopxfr2  6271  relmpt2opab  6288  reldmtpos  6329  dmtpos  6333  dftpos4  6340  tpostpos  6341  iiner  6818  fundmen  7022  nqerf  8644  uzrdgfni  11113  hashfun  11485  homarel  13967  relxpchom  14054  pi1xfrcnv  18659  reldv  19324  dvbsss  19356  rngosn3  21205  vcoprnelem  21248  vcex  21250  eqbrrdva  23232  ustrel  23517  metustrel  23596  txprel  24977  relsset  24986  elfuns  25012  fnsingle  25016  funimage  25025  linedegen  25325  opelopab3  25697  sbcrel  27304  relopabVD  28439  dihvalrel  31538
  Copyright terms: Public domain W3C validator