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

Theorem relen 8553
Description: Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
Assertion
Ref Expression
relen Rel ≈

Proof of Theorem relen
Dummy variables 𝑥 𝑦 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-en 8549 . 2 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
21relopabiv 5658 1 Rel ≈
Colors of variables: wff setvar class
Syntax hints:  wex 1786  Rel wrel 5524  1-1-ontowf1o 6332  cen 8545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-opab 5090  df-xp 5525  df-rel 5526  df-en 8549
This theorem is referenced by:  encv  8556  isfi  8572  enssdom  8573  ener  8595  en1uniel  8621  enfixsn  8668  sbthcl  8682  xpen  8723  pwen  8733  php3  8746  f1finf1o  8816  mapfien2  8939  isnum2  9440  inffien  9556  djuen  9662  djuenun  9663  cdainflem  9680  djulepw  9685  infmap2  9711  fin4i  9791  fin4en1  9802  isfin4p1  9808  enfin2i  9814  fin45  9885  axcc3  9931  engch  10121  hargch  10166  hasheni  13793  pmtrfv  18691  frgpcyg  20385  lbslcic  20650  phpreu  35373  ctbnfien  40196
  Copyright terms: Public domain W3C validator