Theorem reldom 8937

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

Syntax hints:  ∃wex 1802  Rel wrel 5657  –1-1→wf1 6522   ≼ cdom 8929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-opab 5168  df-xp 5658  df-rel 5659  df-dom 8933

This theorem is referenced by:  relsdom  8938  brdomg  8943  brdomi  8944  ctex  8948  domssl  8983  domssr  8984  domtr  8992  undom  9041  xpdom2  9048  xpdom1g  9050  domunsncan  9053  sbth  9073  sbthcl  9075  fodomr  9104  pwdom  9105  domssex  9114  mapdom1  9118  mapdom2  9124  domtrfil  9164  sbthfi  9171  0sdom1dom  9194  1sdom2dom  9202  fineqv  9215  infsdomnn  9249  infn0ALT  9251  elharval  9511  harword  9513  domwdom  9524  unxpwdom  9539  infdifsn  9614  infdiffi  9615  ac10ct  10006  djudom2  10155  djuinf  10160  infdju1  10161  pwdjuidm  10163  djulepw  10164  infdjuabs  10176  infunabs  10177  pwdjudom  10186  infpss  10187  infmap2  10188  fictb  10215  infpssALT  10285  fin34  10362  ttukeylem1  10481  fodomb  10498  wdomac  10499  brdom3  10500  iundom2g  10512  iundom  10514  infxpidm  10534  gchdomtri  10602  pwfseq  10637  pwxpndom2  10638  pwxpndom  10639  pwdjundom  10640  gchdjuidm  10641  gchpwdom  10643  gchaclem  10651  reexALT  12999  hashdomi  14407  1stcrestlem  23570  hauspwdom  23619  ufilen  24048  ovoliunnul  25627  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  nnfoctb  45626  rn1st  45846  meadjiun  47038  caragenunicl  47096