Theorem reldom 8697

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

Syntax hints:  ∃wex 1783  Rel wrel 5585  –1-1→wf1 6415   ≼ cdom 8689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587  df-dom 8693

This theorem is referenced by:  relsdom  8698  brdomg  8703  brdomi  8704  ctex  8708  domtr  8748  undom  8800  xpdom2  8807  xpdom1g  8809  domunsncan  8812  sbth  8833  sbthcl  8835  dom0  8841  fodomr  8864  pwdom  8865  domssex  8874  mapdom1  8878  mapdom2  8884  sbthfi  8942  fineqv  8967  infsdomnn  9005  infn0  9006  elharval  9250  harword  9252  domwdom  9263  unxpwdom  9278  infdifsn  9345  infdiffi  9346  ac10ct  9721  djudom2  9870  djuinf  9875  infdju1  9876  pwdjuidm  9878  djulepw  9879  infdjuabs  9893  infunabs  9894  pwdjudom  9903  infpss  9904  infmap2  9905  fictb  9932  infpssALT  10000  fin34  10077  ttukeylem1  10196  fodomb  10213  wdomac  10214  brdom3  10215  iundom2g  10227  iundom  10229  infxpidm  10249  gchdomtri  10316  pwfseq  10351  pwxpndom2  10352  pwxpndom  10353  pwdjundom  10354  gchdjuidm  10355  gchpwdom  10357  gchaclem  10365  reexALT  12653  hashdomi  14023  1stcrestlem  22511  hauspwdom  22560  ufilen  22989  ovoliunnul  24576  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  nnfoctb  42484  meadjiun  43894  caragenunicl  43952