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 5774	1 ⊢ Rel ≈

Syntax hints:  ∃wex 1779  Rel wrel 5636  –1-1-onto→wf1o 6498   ≈ cen 8892

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 3446  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638  df-en 8896

This theorem is referenced by:  encv  8903  isfi  8924  enssdom  8925  ener  8949  enfixsn  9027  sbthcl  9040  xpen  9081  pwen  9091  f1finf1oOLD  9193  mapfien2  9336  isnum2  9874  inffien  9992  djuen  10099  djuenun  10100  cdainflem  10117  djulepw  10122  infmap2  10146  fin4i  10227  fin4en1  10238  isfin4p1  10244  enfin2i  10250  fin45  10321  axcc3  10367  engch  10557  hargch  10602  hasheni  14289  pmtrfv  19366  frgpcyg  21515  lbslcic  21783  phpreu  37591  ctbnfien  42799