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

Theorem relen 8990
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 8986 . 2 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
21relopabiv 5830 1 Rel ≈
Colors of variables: wff setvar class
Syntax hints:  wex 1779  Rel wrel 5690  1-1-ontowf1o 6560  cen 8982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-en 8986
This theorem is referenced by:  encv  8993  isfi  9016  enssdom  9017  ener  9041  enfixsn  9121  sbthcl  9135  xpen  9180  pwen  9190  php3OLD  9261  f1finf1oOLD  9306  mapfien2  9449  isnum2  9985  inffien  10103  djuen  10210  djuenun  10211  cdainflem  10228  djulepw  10233  infmap2  10257  fin4i  10338  fin4en1  10349  isfin4p1  10355  enfin2i  10361  fin45  10432  axcc3  10478  engch  10668  hargch  10713  hasheni  14387  pmtrfv  19470  frgpcyg  21592  lbslcic  21861  phpreu  37611  ctbnfien  42829
  Copyright terms: Public domain W3C validator