Theorem relen 8874

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

Syntax hints:  ∃wex 1780  Rel wrel 5619  –1-1-onto→wf1o 6480   ≈ cen 8866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621  df-en 8870

This theorem is referenced by:  encv  8877  isfi  8898  enssdom  8899  ener  8923  enfixsn  8999  sbthcl  9012  xpen  9053  pwen  9063  mapfien2  9293  isnum2  9838  inffien  9954  djuen  10061  djuenun  10062  cdainflem  10079  djulepw  10084  infmap2  10108  fin4i  10189  fin4en1  10200  isfin4p1  10206  enfin2i  10212  fin45  10283  axcc3  10329  engch  10519  hargch  10564  hasheni  14255  pmtrfv  19364  frgpcyg  21510  lbslcic  21778  phpreu  37654  ctbnfien  42921