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

Theorem reldom 6871
Description: Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
Assertion
Ref Expression
reldom  |-  Rel  ~<_

Proof of Theorem reldom
Dummy variables  x  y  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-dom 6867 . 2  |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x -1-1-> y }
21relopabi 4813 1  |-  Rel  ~<_
Colors of variables: wff set class
Syntax hints:   E.wex 1530   Rel wrel 4696   -1-1->wf1 5254    ~<_ cdom 6863
This theorem is referenced by:  relsdom  6872  brdomg  6874  brdomi  6875  domtr  6916  undom  6952  xpdom2  6959  xpdom1g  6961  domunsncan  6964  sbth  6983  sbthcl  6985  dom0  6991  fodomr  7014  pwdom  7015  domssex  7024  mapdom1  7028  mapdom2  7034  fineqv  7080  infsdomnn  7120  infn0  7121  elharval  7279  harword  7281  domwdom  7290  unxpwdom  7305  infdifsn  7359  infdiffi  7360  ac10ct  7663  iunfictbso  7743  cdadom1  7814  cdainf  7820  infcda1  7821  pwcdaidm  7823  cdalepw  7824  unctb  7833  infcdaabs  7834  infunabs  7835  infpss  7845  infmap2  7846  fictb  7873  infpssALT  7941  fin34  8018  ttukeylem1  8138  fodomb  8153  wdomac  8154  brdom3  8155  iundom2g  8164  iundom  8166  infxpidm  8186  iunctb  8198  gchdomtri  8253  pwfseq  8288  pwxpndom2  8289  pwxpndom  8290  pwcdandom  8291  gchaclem  8294  gchpwdom  8298  reexALT  10350  hashdomi  11364  cctop  16745  1stcrestlem  17180  2ndcdisj2  17185  dis2ndc  17188  hauspwdom  17229  ufilen  17627  ovoliunnul  18868  uniiccdif  18935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-opab 4080  df-xp 4697  df-rel 4698  df-dom 6867
  Copyright terms: Public domain W3C validator