Theorem relen 8950

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

Syntax hints:  ∃wex 1780  Rel wrel 5681  –1-1-onto→wf1o 6542   ≈ cen 8942

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683  df-en 8946

This theorem is referenced by:  encv  8953  isfi  8978  enssdom  8979  ener  9003  en1unielOLD  9035  enfixsn  9087  sbthcl  9101  xpen  9146  pwen  9156  php3OLD  9230  f1finf1oOLD  9278  mapfien2  9410  isnum2  9946  inffien  10064  djuen  10170  djuenun  10171  cdainflem  10188  djulepw  10193  infmap2  10219  fin4i  10299  fin4en1  10310  isfin4p1  10316  enfin2i  10322  fin45  10393  axcc3  10439  engch  10629  hargch  10674  hasheni  14315  pmtrfv  19368  frgpcyg  21438  lbslcic  21705  phpreu  36935  ctbnfien  42018