Theorem relen 8888

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

Syntax hints:  ∃wex 1780  Rel wrel 5629  –1-1-onto→wf1o 6491   ≈ cen 8880

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-opab 5161  df-xp 5630  df-rel 5631  df-en 8884

This theorem is referenced by:  encv  8891  isfi  8912  enssdomOLD  8914  ener  8938  enfixsn  9014  sbthcl  9027  xpen  9068  pwen  9078  mapfien2  9312  isnum2  9857  inffien  9973  djuen  10080  djuenun  10081  cdainflem  10098  djulepw  10103  infmap2  10127  fin4i  10208  fin4en1  10219  isfin4p1  10225  enfin2i  10231  fin45  10302  axcc3  10348  engch  10539  hargch  10584  hasheni  14271  pmtrfv  19381  frgpcyg  21528  lbslcic  21796  phpreu  37805  ctbnfien  43070