Theorem relen 8900

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

Syntax hints:  ∃wex 1781  Rel wrel 5637  –1-1-onto→wf1o 6499   ≈ cen 8892

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-opab 5163  df-xp 5638  df-rel 5639  df-en 8896

This theorem is referenced by:  encv  8903  isfi  8924  enssdomOLD  8926  ener  8950  enfixsn  9026  sbthcl  9039  xpen  9080  pwen  9090  mapfien2  9324  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  14283  pmtrfv  19393  frgpcyg  21540  lbslcic  21808  phpreu  37855  ctbnfien  43175