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

Theorem reldom 6912
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 6908 . 2  |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x -1-1-> y }
21relopabi 4848 1  |-  Rel  ~<_
Colors of variables: wff set class
Syntax hints:   E.wex 1532   Rel wrel 4731   -1-1->wf1 5289    ~<_ cdom 6904
This theorem is referenced by:  relsdom  6913  brdomg  6915  brdomi  6916  domtr  6957  undom  6993  xpdom2  7000  xpdom1g  7002  domunsncan  7005  sbth  7024  sbthcl  7026  dom0  7032  fodomr  7055  pwdom  7056  domssex  7065  mapdom1  7069  mapdom2  7075  fineqv  7121  infsdomnn  7163  infn0  7164  elharval  7322  harword  7324  domwdom  7333  unxpwdom  7348  infdifsn  7402  infdiffi  7403  ac10ct  7706  iunfictbso  7786  cdadom1  7857  cdainf  7863  infcda1  7864  pwcdaidm  7866  cdalepw  7867  unctb  7876  infcdaabs  7877  infunabs  7878  infpss  7888  infmap2  7889  fictb  7916  infpssALT  7984  fin34  8061  ttukeylem1  8181  fodomb  8196  wdomac  8197  brdom3  8198  iundom2g  8207  iundom  8209  infxpidm  8229  iunctb  8241  gchdomtri  8296  pwfseq  8331  pwxpndom2  8332  pwxpndom  8333  pwcdandom  8334  gchaclem  8337  gchpwdom  8341  reexALT  10395  hashdomi  11409  cctop  16799  1stcrestlem  17234  2ndcdisj2  17239  dis2ndc  17242  hauspwdom  17283  ufilen  17677  ovoliunnul  18919  uniiccdif  18986  ovoliunnfl  25315
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-opab 4115  df-xp 4732  df-rel 4733  df-dom 6908
  Copyright terms: Public domain W3C validator