Theorem reldom 7606

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 7602	. 2 |- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
2	1	relopabi 4981	1 |- Rel ~<_

Syntax hints:   E.wex 1674   Rel wrel 4861   -1-1->wf1 5602   ~<_ cdom 7598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4478  df-xp 4862  df-rel 4863  df-dom 7602

This theorem is referenced by:  relsdom  7607  brdomg  7610  brdomi  7611  domtr  7653  undom  7691  xpdom2  7698  xpdom1g  7700  domunsncan  7703  sbth  7723  sbthcl  7725  dom0  7731  fodomr  7754  pwdom  7755  domssex  7764  mapdom1  7768  mapdom2  7774  fineqv  7818  infsdomnn  7863  infn0  7864  elharval  8109  harword  8111  domwdom  8120  unxpwdom  8135  infdifsn  8193  infdiffi  8194  ac10ct  8496  iunfictbso  8576  cdadom1  8647  cdainf  8653  infcda1  8654  pwcdaidm  8656  cdalepw  8657  unctb  8666  infcdaabs  8667  infunabs  8668  infpss  8678  infmap2  8679  fictb  8706  infpssALT  8774  fin34  8851  ttukeylem1  8970  fodomb  8985  wdomac  8986  brdom3  8987  iundom2g  8996  iundom  8998  infxpidm  9018  iunctb  9030  gchdomtri  9085  pwfseq  9120  pwxpndom2  9121  pwxpndom  9122  pwcdandom  9123  gchpwdom  9126  gchaclem  9134  reexALT  11330  hashdomi  12597  cctop  20076  1stcrestlem  20522  2ndcdisj2  20527  dis2ndc  20530  hauspwdom  20571  ufilen  21000  ovoliunnul  22515  uniiccdif  22591  ovoliunnfl  32028  voliunnfl  32030  volsupnfl  32031  nnfoctb  37422  meadjiun  38409  caragenunicl  38453