Theorem reldom 8739

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

Syntax hints:  ∃wex 1782  Rel wrel 5594  –1-1→wf1 6430   ≼ cdom 8731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596  df-dom 8735

This theorem is referenced by:  relsdom  8740  brdomg  8746  brdomgOLD  8747  brdomi  8748  brdomiOLD  8749  ctex  8753  domtr  8793  undom  8846  undomOLD  8847  xpdom2  8854  xpdom1g  8856  domunsncan  8859  sbth  8880  sbthcl  8882  dom0OLD  8890  fodomr  8915  pwdom  8916  domssex  8925  mapdom1  8929  mapdom2  8935  domtrfil  8978  sbthfi  8985  fineqv  9038  infsdomnn  9075  infn0  9076  elharval  9320  harword  9322  domwdom  9333  unxpwdom  9348  infdifsn  9415  infdiffi  9416  ac10ct  9790  djudom2  9939  djuinf  9944  infdju1  9945  pwdjuidm  9947  djulepw  9948  infdjuabs  9962  infunabs  9963  pwdjudom  9972  infpss  9973  infmap2  9974  fictb  10001  infpssALT  10069  fin34  10146  ttukeylem1  10265  fodomb  10282  wdomac  10283  brdom3  10284  iundom2g  10296  iundom  10298  infxpidm  10318  gchdomtri  10385  pwfseq  10420  pwxpndom2  10421  pwxpndom  10422  pwdjundom  10423  gchdjuidm  10424  gchpwdom  10426  gchaclem  10434  reexALT  12724  hashdomi  14095  1stcrestlem  22603  hauspwdom  22652  ufilen  23081  ovoliunnul  24671  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  nnfoctb  42595  meadjiun  44004  caragenunicl  44062