Theorem relen 8888

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

Syntax hints:  ∃wex 1786  Rel wrel 5623  –1-1-onto→wf1o 6484   ≈ cen 8880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-opab 5135  df-xp 5624  df-rel 5625  df-en 8884

This theorem is referenced by:  encv  8891  isfi  8912  enssdomOLD  8914  ener  8938  enfixsn  9014  sbthcl  9027  xpen  9068  pwen  9078  mapfien2  9312  isnum2  9860  inffien  9976  djuen  10083  djuenun  10084  cdainflem  10101  djulepw  10106  infmap2  10130  fin4i  10211  fin4en1  10222  isfin4p1  10228  enfin2i  10234  fin45  10305  axcc3  10351  engch  10542  hargch  10587  hasheni  14301  pmtrfv  19418  frgpcyg  21548  lbslcic  21816  phpreu  37971  ctbnfien  43263