Theorem reldom 8498

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

Syntax hints:  ∃wex 1781  Rel wrel 5524  –1-1→wf1 6321   ≼ cdom 8490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525  df-rel 5526  df-dom 8494

This theorem is referenced by:  relsdom  8499  brdomg  8502  brdomi  8503  ctex  8507  domtr  8545  undom  8588  xpdom2  8595  xpdom1g  8597  domunsncan  8600  sbth  8621  sbthcl  8623  dom0  8629  fodomr  8652  pwdom  8653  domssex  8662  mapdom1  8666  mapdom2  8672  fineqv  8717  infsdomnn  8763  infn0  8764  elharval  9009  harword  9011  domwdom  9022  unxpwdom  9037  infdifsn  9104  infdiffi  9105  ac10ct  9445  djudom2  9594  djuinf  9599  infdju1  9600  pwdjuidm  9602  djulepw  9603  infdjuabs  9617  infunabs  9618  pwdjudom  9627  infpss  9628  infmap2  9629  fictb  9656  infpssALT  9724  fin34  9801  ttukeylem1  9920  fodomb  9937  wdomac  9938  brdom3  9939  iundom2g  9951  iundom  9953  infxpidm  9973  gchdomtri  10040  pwfseq  10075  pwxpndom2  10076  pwxpndom  10077  pwdjundom  10078  gchdjuidm  10079  gchpwdom  10081  gchaclem  10089  reexALT  12371  hashdomi  13737  1stcrestlem  22057  hauspwdom  22106  ufilen  22535  ovoliunnul  24111  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  nnfoctb  41681  meadjiun  43105  caragenunicl  43163