Theorem relen 8923

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

Syntax hints:  ∃wex 1779  Rel wrel 5643  –1-1-onto→wf1o 6510   ≈ cen 8915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645  df-en 8919

This theorem is referenced by:  encv  8926  isfi  8947  enssdom  8948  ener  8972  enfixsn  9050  sbthcl  9063  xpen  9104  pwen  9114  f1finf1oOLD  9217  mapfien2  9360  isnum2  9898  inffien  10016  djuen  10123  djuenun  10124  cdainflem  10141  djulepw  10146  infmap2  10170  fin4i  10251  fin4en1  10262  isfin4p1  10268  enfin2i  10274  fin45  10345  axcc3  10391  engch  10581  hargch  10626  hasheni  14313  pmtrfv  19382  frgpcyg  21483  lbslcic  21750  phpreu  37598  ctbnfien  42806