Theorem relen 8988

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 8984	. 2 ⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
2	1	relopabiv 5832	1 ⊢ Rel ≈

Syntax hints:  ∃wex 1775  Rel wrel 5693  –1-1-onto→wf1o 6561   ≈ cen 8980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-opab 5210  df-xp 5694  df-rel 5695  df-en 8984

This theorem is referenced by:  encv  8991  isfi  9014  enssdom  9015  ener  9039  enfixsn  9119  sbthcl  9133  xpen  9178  pwen  9188  php3OLD  9258  f1finf1oOLD  9303  mapfien2  9446  isnum2  9982  inffien  10100  djuen  10207  djuenun  10208  cdainflem  10225  djulepw  10230  infmap2  10254  fin4i  10335  fin4en1  10346  isfin4p1  10352  enfin2i  10358  fin45  10429  axcc3  10475  engch  10665  hargch  10710  hasheni  14383  pmtrfv  19484  frgpcyg  21609  lbslcic  21878  phpreu  37590  ctbnfien  42805