Theorem relen 8877

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

Syntax hints:  ∃wex 1779  Rel wrel 5624  –1-1-onto→wf1o 6481   ≈ cen 8869

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 3438  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626  df-en 8873

This theorem is referenced by:  encv  8880  isfi  8901  enssdom  8902  ener  8926  enfixsn  9003  sbthcl  9016  xpen  9057  pwen  9067  mapfien2  9299  isnum2  9841  inffien  9957  djuen  10064  djuenun  10065  cdainflem  10082  djulepw  10087  infmap2  10111  fin4i  10192  fin4en1  10203  isfin4p1  10209  enfin2i  10215  fin45  10286  axcc3  10332  engch  10522  hargch  10567  hasheni  14255  pmtrfv  19331  frgpcyg  21480  lbslcic  21748  phpreu  37594  ctbnfien  42801