Theorem reldom 8881

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

Syntax hints:  ∃wex 1780  Rel wrel 5624  –1-1→wf1 6483   ≼ cdom 8873

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-opab 5156  df-xp 5625  df-rel 5626  df-dom 8877

This theorem is referenced by:  relsdom  8882  brdomg  8887  brdomi  8888  ctex  8892  domssl  8927  domssr  8928  domtr  8936  undom  8985  xpdom2  8992  xpdom1g  8994  domunsncan  8997  sbth  9017  sbthcl  9019  fodomr  9048  pwdom  9049  domssex  9058  mapdom1  9062  mapdom2  9068  domtrfil  9108  sbthfi  9115  0sdom1dom  9137  1sdom2dom  9145  fineqv  9158  infsdomnn  9192  infn0ALT  9194  elharval  9454  harword  9456  domwdom  9467  unxpwdom  9482  infdifsn  9554  infdiffi  9555  ac10ct  9932  djudom2  10082  djuinf  10087  infdju1  10088  pwdjuidm  10090  djulepw  10091  infdjuabs  10103  infunabs  10104  pwdjudom  10113  infpss  10114  infmap2  10115  fictb  10142  infpssALT  10211  fin34  10288  ttukeylem1  10407  fodomb  10424  wdomac  10425  brdom3  10426  iundom2g  10438  iundom  10440  infxpidm  10460  gchdomtri  10527  pwfseq  10562  pwxpndom2  10563  pwxpndom  10564  pwdjundom  10565  gchdjuidm  10566  gchpwdom  10568  gchaclem  10576  reexALT  12884  hashdomi  14289  1stcrestlem  23368  hauspwdom  23417  ufilen  23846  ovoliunnul  25436  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  nnfoctb  45169  rn1st  45394  meadjiun  46588  caragenunicl  46646