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

Definition df-rel 4888
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5324 and dfrel3 5331. (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 4886 . 2  wff  Rel  A
3 cvv 2958 . . . 4  class  _V
43, 3cxp 4879 . . 3  class  ( _V 
X.  _V )
51, 4wss 3322 . 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  4918  releq  4962  nfrel  4965  relss  4966  ssrel  4967  elrel  4981  relsn  4982  relxp  4986  relun  4994  reliun  4998  reliin  4999  rel0  5002  relopabi  5003  relop  5026  eqbrrdva  5045  elreldm  5097  issref  5250  cnvcnv  5326  relrelss  5396  cnviin  5412  nfunv  5487  dff3  5885  oprabss  6162  relmptopab  6295  1st2nd  6396  1stdm  6397  releldm2  6400  exopxfr2  6414  relmpt2opab  6432  reldmtpos  6490  dmtpos  6494  dftpos4  6501  tpostpos  6502  iiner  6979  fundmen  7183  nqerf  8812  uzrdgfni  11303  hashfun  11705  homarel  14196  relxpchom  14283  ustrel  18246  utop2nei  18285  utop3cls  18286  metustrelOLD  18590  metustrel  18591  pi1xfrcnv  19087  reldv  19762  dvbsss  19794  rngosn3  22019  vcoprnelem  22062  vcex  22064  metideq  24293  metider  24294  pstmfval  24296  txprel  25729  relsset  25738  elfuns  25765  fnsingle  25769  funimage  25778  linedegen  26082  mblfinlem1  26255  opelopab3  26432  sbcrel  27971  relopabVD  29087  dihvalrel  32151
  Copyright terms: Public domain W3C validator