Theorem reldom 8875

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 8871	. 2 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
2	1	relopabiv 5760	1 ⊢ Rel ≼

Syntax hints:  ∃wex 1780  Rel wrel 5621  –1-1→wf1 6478   ≼ cdom 8867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-opab 5154  df-xp 5622  df-rel 5623  df-dom 8871

This theorem is referenced by:  relsdom  8876  brdomg  8881  brdomi  8882  ctex  8886  domssl  8920  domssr  8921  domtr  8929  undom  8978  xpdom2  8985  xpdom1g  8987  domunsncan  8990  sbth  9010  sbthcl  9012  fodomr  9041  pwdom  9042  domssex  9051  mapdom1  9055  mapdom2  9061  domtrfil  9101  sbthfi  9108  0sdom1dom  9130  1sdom2dom  9138  fineqv  9151  infsdomnn  9185  infn0ALT  9187  elharval  9447  harword  9449  domwdom  9460  unxpwdom  9475  infdifsn  9547  infdiffi  9548  ac10ct  9922  djudom2  10072  djuinf  10077  infdju1  10078  pwdjuidm  10080  djulepw  10081  infdjuabs  10093  infunabs  10094  pwdjudom  10103  infpss  10104  infmap2  10105  fictb  10132  infpssALT  10201  fin34  10278  ttukeylem1  10397  fodomb  10414  wdomac  10415  brdom3  10416  iundom2g  10428  iundom  10430  infxpidm  10450  gchdomtri  10517  pwfseq  10552  pwxpndom2  10553  pwxpndom  10554  pwdjundom  10555  gchdjuidm  10556  gchpwdom  10558  gchaclem  10566  reexALT  12879  hashdomi  14284  1stcrestlem  23365  hauspwdom  23414  ufilen  23843  ovoliunnul  25433  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  nnfoctb  45084  rn1st  45309  meadjiun  46503  caragenunicl  46561