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

Theorem reldom 8127
 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 8123 . 2 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
21relopabi 5401 1 Rel ≼
 Colors of variables: wff setvar class Syntax hints:  ∃wex 1853  Rel wrel 5271  –1-1→wf1 6046   ≼ cdom 8119 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-opab 4865  df-xp 5272  df-rel 5273  df-dom 8123 This theorem is referenced by:  relsdom  8128  brdomg  8131  brdomi  8132  domtr  8174  undom  8213  xpdom2  8220  xpdom1g  8222  domunsncan  8225  sbth  8245  sbthcl  8247  dom0  8253  fodomr  8276  pwdom  8277  domssex  8286  mapdom1  8290  mapdom2  8296  fineqv  8340  infsdomnn  8386  infn0  8387  elharval  8633  harword  8635  domwdom  8644  unxpwdom  8659  infdifsn  8727  infdiffi  8728  ac10ct  9047  iunfictbso  9127  cdadom1  9200  cdainf  9206  infcda1  9207  pwcdaidm  9209  cdalepw  9210  unctb  9219  infcdaabs  9220  infunabs  9221  infpss  9231  infmap2  9232  fictb  9259  infpssALT  9327  fin34  9404  ttukeylem1  9523  fodomb  9540  wdomac  9541  brdom3  9542  iundom2g  9554  iundom  9556  infxpidm  9576  iunctb  9588  gchdomtri  9643  pwfseq  9678  pwxpndom2  9679  pwxpndom  9680  pwcdandom  9681  gchpwdom  9684  gchaclem  9692  reexALT  12019  hashdomi  13361  1stcrestlem  21457  2ndcdisj2  21462  dis2ndc  21465  hauspwdom  21506  ufilen  21935  ovoliunnul  23475  uniiccdif  23546  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  nnfoctb  39712  meadjiun  41186  caragenunicl  41244
 Copyright terms: Public domain W3C validator