Theorem reldom 7847

Description: Dominance is a relation. (Contributed by NM, 28-Mar-1998.)

Assertion

Ref	Expression
reldom	⊢ Rel ≼

Proof of Theorem reldom

Dummy variables 𝑥 𝑦 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-dom 7843	. 2 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
2	1	relopabi 5167	1 ⊢ Rel ≼

Syntax hints:  ∃wex 1695  Rel wrel 5043  –1-1→wf1 5801   ≼ cdom 7839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-xp 5044  df-rel 5045  df-dom 7843

This theorem is referenced by:  relsdom  7848  brdomg  7851  brdomi  7852  domtr  7895  undom  7933  xpdom2  7940  xpdom1g  7942  domunsncan  7945  sbth  7965  sbthcl  7967  dom0  7973  fodomr  7996  pwdom  7997  domssex  8006  mapdom1  8010  mapdom2  8016  fineqv  8060  infsdomnn  8106  infn0  8107  elharval  8351  harword  8353  domwdom  8362  unxpwdom  8377  infdifsn  8437  infdiffi  8438  ac10ct  8740  iunfictbso  8820  cdadom1  8891  cdainf  8897  infcda1  8898  pwcdaidm  8900  cdalepw  8901  unctb  8910  infcdaabs  8911  infunabs  8912  infpss  8922  infmap2  8923  fictb  8950  infpssALT  9018  fin34  9095  ttukeylem1  9214  fodomb  9229  wdomac  9230  brdom3  9231  iundom2g  9241  iundom  9243  infxpidm  9263  iunctb  9275  gchdomtri  9330  pwfseq  9365  pwxpndom2  9366  pwxpndom  9367  pwcdandom  9368  gchpwdom  9371  gchaclem  9379  reexALT  11702  hashdomi  13030  1stcrestlem  21065  2ndcdisj2  21070  dis2ndc  21073  hauspwdom  21114  ufilen  21544  ovoliunnul  23082  uniiccdif  23152  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  nnfoctb  38238  meadjiun  39359  caragenunicl  39414