Theorem relen 8898

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

Syntax hints:  ∃wex 1781  Rel wrel 5636  –1-1-onto→wf1o 6497   ≈ cen 8890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638  df-en 8894

This theorem is referenced by:  encv  8901  isfi  8922  enssdomOLD  8924  ener  8948  enfixsn  9024  sbthcl  9037  xpen  9078  pwen  9088  mapfien2  9322  isnum2  9869  inffien  9985  djuen  10092  djuenun  10093  cdainflem  10110  djulepw  10115  infmap2  10139  fin4i  10220  fin4en1  10231  isfin4p1  10237  enfin2i  10243  fin45  10314  axcc3  10360  engch  10551  hargch  10596  hasheni  14310  pmtrfv  19427  frgpcyg  21553  lbslcic  21821  phpreu  37925  ctbnfien  43246