Theorem relen 8926

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

Syntax hints:  ∃wex 1779  Rel wrel 5646  –1-1-onto→wf1o 6513   ≈ cen 8918

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648  df-en 8922

This theorem is referenced by:  encv  8929  isfi  8950  enssdom  8951  ener  8975  enfixsn  9055  sbthcl  9069  xpen  9110  pwen  9120  f1finf1oOLD  9224  mapfien2  9367  isnum2  9905  inffien  10023  djuen  10130  djuenun  10131  cdainflem  10148  djulepw  10153  infmap2  10177  fin4i  10258  fin4en1  10269  isfin4p1  10275  enfin2i  10281  fin45  10352  axcc3  10398  engch  10588  hargch  10633  hasheni  14320  pmtrfv  19389  frgpcyg  21490  lbslcic  21757  phpreu  37605  ctbnfien  42813