Theorem relen 8960

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

This proof depends on syntax axioms:  ∃wex 1812  Rel wrel 5660  –1-1-onto→wf1o 6532   ≈ cen 8952

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-opab 5168  df-xp 5661  df-rel 5662  df-en 8956

This theorem is used by:  encv  8963  isfi  8984  enssdomOLD  8986  ener  9010  enfixsn  9087  sbthcl  9100  xpen  9141  pwen  9151  mapfien2  9382  isnum2  9953  inffien  10069  djuen  10175  djuenun  10176  cdainflem  10193  djulepw  10198  infmap2  10222  fin4i  10303  fin4en1  10314  isfin4p1  10320  enfin2i  10326  fin45  10397  axcc3  10443  engch  10640  hargch  10685  hasheni  14415  pmtrfv  19582  frgpcyg  21789  lbslcic  22057  kardenir  35687  phpreu  38361  ctbnfien  43662