Theorem reldom 7961

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

Syntax hints:  ∃wex 1704  Rel wrel 5119  –1-1→wf1 5885   ≼ cdom 7953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120  df-rel 5121  df-dom 7957

This theorem is referenced by:  relsdom  7962  brdomg  7965  brdomi  7966  domtr  8009  undom  8048  xpdom2  8055  xpdom1g  8057  domunsncan  8060  sbth  8080  sbthcl  8082  dom0  8088  fodomr  8111  pwdom  8112  domssex  8121  mapdom1  8125  mapdom2  8131  fineqv  8175  infsdomnn  8221  infn0  8222  elharval  8468  harword  8470  domwdom  8479  unxpwdom  8494  infdifsn  8554  infdiffi  8555  ac10ct  8857  iunfictbso  8937  cdadom1  9008  cdainf  9014  infcda1  9015  pwcdaidm  9017  cdalepw  9018  unctb  9027  infcdaabs  9028  infunabs  9029  infpss  9039  infmap2  9040  fictb  9067  infpssALT  9135  fin34  9212  ttukeylem1  9331  fodomb  9348  wdomac  9349  brdom3  9350  iundom2g  9362  iundom  9364  infxpidm  9384  iunctb  9396  gchdomtri  9451  pwfseq  9486  pwxpndom2  9487  pwxpndom  9488  pwcdandom  9489  gchpwdom  9492  gchaclem  9500  reexALT  11826  hashdomi  13169  1stcrestlem  21255  2ndcdisj2  21260  dis2ndc  21263  hauspwdom  21304  ufilen  21734  ovoliunnul  23275  uniiccdif  23346  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  nnfoctb  39213  meadjiun  40683  caragenunicl  40738