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

Theorem reldom 6869
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 6865 . 2  |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x -1-1-> y }
21relopabi 4811 1  |-  Rel  ~<_
Colors of variables: wff set class
Syntax hints:   E.wex 1528   Rel wrel 4694   -1-1->wf1 5252    ~<_ cdom 6861
This theorem is referenced by:  relsdom  6870  brdomg  6872  brdomi  6873  domtr  6914  undom  6950  xpdom2  6957  xpdom1g  6959  domunsncan  6962  sbth  6981  sbthcl  6983  dom0  6989  fodomr  7012  pwdom  7013  domssex  7022  mapdom1  7026  mapdom2  7032  fineqv  7078  infsdomnn  7118  infn0  7119  elharval  7277  harword  7279  domwdom  7288  unxpwdom  7303  infdifsn  7357  infdiffi  7358  ac10ct  7661  iunfictbso  7741  cdadom1  7812  cdainf  7818  infcda1  7819  pwcdaidm  7821  cdalepw  7822  unctb  7831  infcdaabs  7832  infunabs  7833  infpss  7843  infmap2  7844  fictb  7871  infpssALT  7939  fin34  8016  ttukeylem1  8136  fodomb  8151  wdomac  8152  brdom3  8153  iundom2g  8162  iundom  8164  infxpidm  8184  iunctb  8196  gchdomtri  8251  pwfseq  8286  pwxpndom2  8287  pwxpndom  8288  pwcdandom  8289  gchaclem  8292  gchpwdom  8296  reexALT  10348  hashdomi  11362  cctop  16743  1stcrestlem  17178  2ndcdisj2  17183  dis2ndc  17186  hauspwdom  17227  ufilen  17625  ovoliunnul  18866  uniiccdif  18933
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695  df-rel 4696  df-dom 6865
  Copyright terms: Public domain W3C validator