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

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

Proof of Theorem relen
Dummy variables  x  y  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-en 7536 . 2  |-  ~~  =  { <. x ,  y
>.  |  E. f 
f : x -1-1-onto-> y }
21relopabi 5137 1  |-  Rel  ~~
Colors of variables: wff setvar class
Syntax hints:   E.wex 1613   Rel wrel 5013   -1-1-onto->wf1o 5593    ~~ cen 7532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-opab 4516  df-xp 5014  df-rel 5015  df-en 7536
This theorem is referenced by:  encv  7543  isfi  7558  enssdom  7559  ener  7581  en1uniel  7606  enfixsn  7645  sbthcl  7658  xpen  7699  pwen  7709  php3  7722  f1finf1o  7765  mapfien2  7886  isnum2  8343  inffien  8461  cdaen  8570  cdaenun  8571  cdainflem  8588  cdalepw  8593  infmap2  8615  fin4i  8695  fin4en1  8706  isfin4-3  8712  enfin2i  8718  fin45  8789  axcc3  8835  engch  9023  hargch  9068  hasheni  12424  pmtrfv  16604  frgpcyg  18739  lbslcic  19003  ctbnfien  30935  mapfien2OLD  31225
  Copyright terms: Public domain W3C validator