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

Theorem relen 8944
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 8940 . 2 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
21relopabiv 5821 1 Rel ≈
Colors of variables: wff setvar class
Syntax hints:  wex 1782  Rel wrel 5682  1-1-ontowf1o 6543  cen 8936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684  df-en 8940
This theorem is referenced by:  encv  8947  isfi  8972  enssdom  8973  ener  8997  en1unielOLD  9029  enfixsn  9081  sbthcl  9095  xpen  9140  pwen  9150  php3OLD  9224  f1finf1oOLD  9272  mapfien2  9404  isnum2  9940  inffien  10058  djuen  10164  djuenun  10165  cdainflem  10182  djulepw  10187  infmap2  10213  fin4i  10293  fin4en1  10304  isfin4p1  10310  enfin2i  10316  fin45  10387  axcc3  10433  engch  10623  hargch  10668  hasheni  14308  pmtrfv  19320  frgpcyg  21129  lbslcic  21396  phpreu  36472  ctbnfien  41556
  Copyright terms: Public domain W3C validator