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

Theorem relen 7912
 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 7908 . 2 ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1-onto𝑦}
21relopabi 5210 1 Rel ≈
 Colors of variables: wff setvar class Syntax hints:  ∃wex 1701  Rel wrel 5084  –1-1-onto→wf1o 5851   ≈ cen 7904 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-opab 4679  df-xp 5085  df-rel 5086  df-en 7908 This theorem is referenced by:  encv  7915  isfi  7931  enssdom  7932  ener  7954  enerOLD  7955  en1uniel  7980  enfixsn  8021  sbthcl  8034  xpen  8075  pwen  8085  php3  8098  f1finf1o  8139  mapfien2  8266  isnum2  8723  inffien  8838  cdaen  8947  cdaenun  8948  cdainflem  8965  cdalepw  8970  infmap2  8992  fin4i  9072  fin4en1  9083  isfin4-3  9089  enfin2i  9095  fin45  9166  axcc3  9212  engch  9402  hargch  9447  hasheni  13084  pmtrfv  17804  frgpcyg  19854  lbslcic  20112  phpreu  33060  ctbnfien  36897
 Copyright terms: Public domain W3C validator