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

Theorem relen 8169
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 8165 . 2 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
21relopabi 5416 1 Rel ≈
Colors of variables: wff setvar class
Syntax hints:  wex 1874  Rel wrel 5284  1-1-ontowf1o 6069  cen 8161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-opab 4874  df-xp 5285  df-rel 5286  df-en 8165
This theorem is referenced by:  encv  8172  isfi  8188  enssdom  8189  ener  8211  en1uniel  8236  enfixsn  8280  sbthcl  8293  xpen  8334  pwen  8344  php3  8357  f1finf1o  8398  mapfien2  8525  isnum2  9026  inffien  9141  cdaen  9252  cdaenun  9253  cdainflem  9270  cdalepw  9275  infmap2  9297  fin4i  9377  fin4en1  9388  isfin4-3  9394  enfin2i  9400  fin45  9471  axcc3  9517  engch  9707  hargch  9752  hasheni  13345  pmtrfv  18149  frgpcyg  20208  lbslcic  20470  phpreu  33838  ctbnfien  38084
  Copyright terms: Public domain W3C validator