Theorem reldom 7512

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

Syntax hints:   E.wex 1591   Rel wrel 4997   -1-1->wf1 5576   ~<_ cdom 7504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-opab 4499  df-xp 4998  df-rel 4999  df-dom 7508

This theorem is referenced by:  relsdom  7513  brdomg  7516  brdomi  7517  domtr  7558  undom  7595  xpdom2  7602  xpdom1g  7604  domunsncan  7607  sbth  7627  sbthcl  7629  dom0  7635  fodomr  7658  pwdom  7659  domssex  7668  mapdom1  7672  mapdom2  7678  fineqv  7725  infsdomnn  7770  infn0  7771  elharval  7978  harword  7980  domwdom  7989  unxpwdom  8004  infdifsn  8062  infdiffi  8063  ac10ct  8404  iunfictbso  8484  cdadom1  8555  cdainf  8561  infcda1  8562  pwcdaidm  8564  cdalepw  8565  unctb  8574  infcdaabs  8575  infunabs  8576  infpss  8586  infmap2  8587  fictb  8614  infpssALT  8682  fin34  8759  ttukeylem1  8878  fodomb  8893  wdomac  8894  brdom3  8895  iundom2g  8904  iundom  8906  infxpidm  8926  iunctb  8938  gchdomtri  8996  pwfseq  9031  pwxpndom2  9032  pwxpndom  9033  pwcdandom  9034  gchpwdom  9037  gchaclem  9045  reexALT  11203  hashdomi  12403  cctop  19266  1stcrestlem  19712  2ndcdisj2  19717  dis2ndc  19720  hauspwdom  19761  ufilen  20159  ovoliunnul  21646  uniiccdif  21715  ovoliunnfl  29620  voliunnfl  29622  volsupnfl  29623