Theorem reldom 8228

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

Syntax hints:  ∃wex 1880  Rel wrel 5347  –1-1→wf1 6120   ≼ cdom 8220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-opab 4936  df-xp 5348  df-rel 5349  df-dom 8224

This theorem is referenced by:  relsdom  8229  brdomg  8232  brdomi  8233  ctex  8237  domtr  8275  undom  8317  xpdom2  8324  xpdom1g  8326  domunsncan  8329  sbth  8349  sbthcl  8351  dom0  8357  fodomr  8380  pwdom  8381  domssex  8390  mapdom1  8394  mapdom2  8400  fineqv  8444  infsdomnn  8490  infn0  8491  elharval  8737  harword  8739  domwdom  8748  unxpwdom  8763  infdifsn  8831  infdiffi  8832  ac10ct  9170  iunfictbso  9250  cdadom1  9323  cdainf  9329  infcda1  9330  pwcdaidm  9332  cdalepw  9333  unctb  9342  infcdaabs  9343  infunabs  9344  infpss  9354  infmap2  9355  fictb  9382  infpssALT  9450  fin34  9527  ttukeylem1  9646  fodomb  9663  wdomac  9664  brdom3  9665  iundom2g  9677  iundom  9679  infxpidm  9699  iunctb  9711  gchdomtri  9766  pwfseq  9801  pwxpndom2  9802  pwxpndom  9803  pwcdandom  9804  gchpwdom  9807  gchaclem  9815  reexALT  12106  hashdomi  13459  1stcrestlem  21626  2ndcdisj2  21631  dis2ndc  21634  hauspwdom  21675  ufilen  22104  ovoliunnul  23673  uniiccdif  23744  ovoliunnfl  33995  voliunnfl  33997  volsupnfl  33998  nnfoctb  40030  meadjiun  41474  caragenunicl  41532