Theorem reldom 8950

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

Syntax hints:  ∃wex 1809  Rel wrel 5668  –1-1→wf1 6535   ≼ cdom 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-opab 5175  df-xp 5669  df-rel 5670  df-dom 8946

This theorem is referenced by:  relsdom  8951  brdomg  8956  brdomi  8957  ctex  8961  domssl  8996  domssr  8997  domtr  9005  undom  9054  xpdom2  9061  xpdom1g  9063  domunsncan  9066  sbth  9086  sbthcl  9088  fodomr  9117  pwdom  9118  domssex  9127  mapdom1  9131  mapdom2  9137  domtrfil  9177  sbthfi  9184  0sdom1dom  9207  1sdom2dom  9215  fineqv  9228  infsdomnn  9262  infn0ALT  9264  elharval  9524  harword  9526  domwdom  9537  unxpwdom  9552  infdifsn  9627  infdiffi  9628  ac10ct  10019  djudom2  10168  djuinf  10173  infdju1  10174  pwdjuidm  10176  djulepw  10177  infdjuabs  10189  infunabs  10190  pwdjudom  10199  infpss  10200  infmap2  10201  fictb  10228  infpssALT  10298  fin34  10375  ttukeylem1  10494  fodomb  10511  wdomac  10512  brdom3  10513  iundom2g  10525  iundom  10527  infxpidm  10547  gchdomtri  10615  pwfseq  10650  pwxpndom2  10651  pwxpndom  10652  pwdjundom  10653  gchdjuidm  10654  gchpwdom  10656  gchaclem  10664  reexALT  13009  hashdomi  14418  1stcrestlem  23590  hauspwdom  23639  ufilen  24068  ovoliunnul  25647  karddom  35552  ovoliunnfl  38291  voliunnfl  38293  volsupnfl  38294  nnfoctb  45748  rn1st  45968  meadjiun  47160  caragenunicl  47218