Theorem relen 8990

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

Syntax hints:  ∃wex 1779  Rel wrel 5690  –1-1-onto→wf1o 6560   ≈ cen 8982

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-en 8986

This theorem is referenced by:  encv  8993  isfi  9016  enssdom  9017  ener  9041  enfixsn  9121  sbthcl  9135  xpen  9180  pwen  9190  php3OLD  9261  f1finf1oOLD  9306  mapfien2  9449  isnum2  9985  inffien  10103  djuen  10210  djuenun  10211  cdainflem  10228  djulepw  10233  infmap2  10257  fin4i  10338  fin4en1  10349  isfin4p1  10355  enfin2i  10361  fin45  10432  axcc3  10478  engch  10668  hargch  10713  hasheni  14387  pmtrfv  19470  frgpcyg  21592  lbslcic  21861  phpreu  37611  ctbnfien  42829