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

Definition df-rel 4885
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5321 and dfrel3 5328. (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 4883 . 2  wff  Rel  A
3 cvv 2956 . . . 4  class  _V
43, 3cxp 4876 . . 3  class  ( _V 
X.  _V )
51, 4wss 3320 . 2  wff  A  C_  ( _V  X.  _V )
62, 5wb 177 1  wff  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
Colors of variables: wff set class
This definition is referenced by:  brrelex12  4915  releq  4959  nfrel  4962  relss  4963  ssrel  4964  elrel  4978  relsn  4979  relxp  4983  relun  4991  reliun  4995  reliin  4996  rel0  4999  relopabi  5000  relop  5023  eqbrrdva  5042  elreldm  5094  issref  5247  cnvcnv  5323  relrelss  5393  cnviin  5409  nfunv  5484  dff3  5882  oprabss  6159  relmptopab  6292  1st2nd  6393  1stdm  6394  releldm2  6397  exopxfr2  6411  relmpt2opab  6429  reldmtpos  6487  dmtpos  6491  dftpos4  6498  tpostpos  6499  iiner  6976  fundmen  7180  nqerf  8807  uzrdgfni  11298  hashfun  11700  homarel  14191  relxpchom  14278  ustrel  18241  utop2nei  18280  utop3cls  18281  metustrelOLD  18585  metustrel  18586  pi1xfrcnv  19082  reldv  19757  dvbsss  19789  rngosn3  22014  vcoprnelem  22057  vcex  22059  metideq  24288  metider  24289  pstmfval  24291  txprel  25724  relsset  25733  elfuns  25760  fnsingle  25764  funimage  25773  linedegen  26077  mblfinlem1  26243  opelopab3  26418  sbcrel  27957  relopabVD  29013  dihvalrel  32077
  Copyright terms: Public domain W3C validator