Theorem reldom 7559

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.

Step	Hyp	Ref	Expression
1		df-dom 7555	. 2 |- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
2	1	relopabi 4947	1 |- Rel ~<_

Syntax hints:   E.wex 1633   Rel wrel 4827   -1-1->wf1 5565   ~<_ cdom 7551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-opab 4453  df-xp 4828  df-rel 4829  df-dom 7555

This theorem is referenced by:  relsdom  7560  brdomg  7563  brdomi  7564  domtr  7605  undom  7642  xpdom2  7649  xpdom1g  7651  domunsncan  7654  sbth  7674  sbthcl  7676  dom0  7682  fodomr  7705  pwdom  7706  domssex  7715  mapdom1  7719  mapdom2  7725  fineqv  7769  infsdomnn  7814  infn0  7815  elharval  8022  harword  8024  domwdom  8033  unxpwdom  8048  infdifsn  8105  infdiffi  8106  ac10ct  8446  iunfictbso  8526  cdadom1  8597  cdainf  8603  infcda1  8604  pwcdaidm  8606  cdalepw  8607  unctb  8616  infcdaabs  8617  infunabs  8618  infpss  8628  infmap2  8629  fictb  8656  infpssALT  8724  fin34  8801  ttukeylem1  8920  fodomb  8935  wdomac  8936  brdom3  8937  iundom2g  8946  iundom  8948  infxpidm  8968  iunctb  8980  gchdomtri  9036  pwfseq  9071  pwxpndom2  9072  pwxpndom  9073  pwcdandom  9074  gchpwdom  9077  gchaclem  9085  reexALT  11258  hashdomi  12494  cctop  19797  1stcrestlem  20243  2ndcdisj2  20248  dis2ndc  20251  hauspwdom  20292  ufilen  20721  ovoliunnul  22208  uniiccdif  22277  ovoliunnfl  31408  voliunnfl  31410  volsupnfl  31411