Theorem relen 8932

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.

Step	Hyp	Ref	Expression
1		df-en 8928	. 2 ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
2	1	relopabiv 5793	1 ⊢ Rel ≈

Syntax hints:  ∃wex 1799  Rel wrel 5652  –1-1-onto→wf1o 6520   ≈ cen 8924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-opab 5163  df-xp 5653  df-rel 5654  df-en 8928

This theorem is referenced by:  encv  8935  isfi  8956  enssdomOLD  8958  ener  8982  enfixsn  9058  sbthcl  9071  xpen  9112  pwen  9122  mapfien2  9355  isnum2  9903  inffien  10019  djuen  10126  djuenun  10127  cdainflem  10144  djulepw  10149  infmap2  10173  fin4i  10255  fin4en1  10266  isfin4p1  10272  enfin2i  10278  fin45  10349  axcc3  10395  engch  10586  hargch  10631  hasheni  14361  pmtrfv  19492  frgpcyg  21625  lbslcic  21893  phpreu  38103  ctbnfien  43395