MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldom Structured version   Visualization version   GIF version

Theorem reldom 8195
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.
StepHypRef Expression
1 df-dom 8191 . 2 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
21relopabi 5444 1 Rel ≼
Colors of variables: wff setvar class
Syntax hints:  wex 1859  Rel wrel 5313  1-1wf1 6095  cdom 8187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-opab 4903  df-xp 5314  df-rel 5315  df-dom 8191
This theorem is referenced by:  relsdom  8196  brdomg  8199  brdomi  8200  domtr  8242  undom  8284  xpdom2  8291  xpdom1g  8293  domunsncan  8296  sbth  8316  sbthcl  8318  dom0  8324  fodomr  8347  pwdom  8348  domssex  8357  mapdom1  8361  mapdom2  8367  fineqv  8411  infsdomnn  8457  infn0  8458  elharval  8704  harword  8706  domwdom  8715  unxpwdom  8730  infdifsn  8798  infdiffi  8799  ac10ct  9137  iunfictbso  9217  cdadom1  9290  cdainf  9296  infcda1  9297  pwcdaidm  9299  cdalepw  9300  unctb  9309  infcdaabs  9310  infunabs  9311  infpss  9321  infmap2  9322  fictb  9349  infpssALT  9417  fin34  9494  ttukeylem1  9613  fodomb  9630  wdomac  9631  brdom3  9632  iundom2g  9644  iundom  9646  infxpidm  9666  iunctb  9678  gchdomtri  9733  pwfseq  9768  pwxpndom2  9769  pwxpndom  9770  pwcdandom  9771  gchpwdom  9774  gchaclem  9782  reexALT  12036  hashdomi  13383  1stcrestlem  21465  2ndcdisj2  21470  dis2ndc  21473  hauspwdom  21514  ufilen  21943  ovoliunnul  23484  uniiccdif  23555  ovoliunnfl  33761  voliunnfl  33763  volsupnfl  33764  nnfoctb  39703  meadjiun  41159  caragenunicl  41217
  Copyright terms: Public domain W3C validator