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

Theorem reldom 8504
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 8500 . 2 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
21relopabi 5693 1 Rel ≼
Colors of variables: wff setvar class
Syntax hints:  wex 1773  Rel wrel 5559  1-1wf1 6349  cdom 8496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-opab 5126  df-xp 5560  df-rel 5561  df-dom 8500
This theorem is referenced by:  relsdom  8505  brdomg  8508  brdomi  8509  ctex  8513  domtr  8551  undom  8594  xpdom2  8601  xpdom1g  8603  domunsncan  8606  sbth  8626  sbthcl  8628  dom0  8634  fodomr  8657  pwdom  8658  domssex  8667  mapdom1  8671  mapdom2  8677  fineqv  8722  infsdomnn  8768  infn0  8769  elharval  9016  harword  9018  domwdom  9027  unxpwdom  9042  infdifsn  9109  infdiffi  9110  ac10ct  9449  djudom2  9598  djuinf  9603  infdju1  9604  pwdjuidm  9606  djulepw  9607  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  12373  hashdomi  13731  1stcrestlem  21976  hauspwdom  22025  ufilen  22454  ovoliunnul  24023  ovoliunnfl  34801  voliunnfl  34803  volsupnfl  34804  nnfoctb  41174  meadjiun  42614  caragenunicl  42672
  Copyright terms: Public domain W3C validator