Theorem relen 8989

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

This proof depends on syntax axioms:  ∃wex 1811  Rel wrel 5659  –1-1-onto→wf1o 6545   ≈ cen 8981

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-opab 5170  df-xp 5660  df-rel 5661  df-en 8985

This theorem is used by:  encv  8992  isfi  9013  enssdomOLD  9015  ener  9039  enfixsn  9116  sbthcl  9129  xpen  9170  pwen  9180  mapfien2  9411  isnum2  10036  inffien  10152  djuen  10258  djuenun  10259  cdainflem  10276  djulepw  10281  infmap2  10305  fin4i  10386  fin4en1  10397  isfin4p1  10403  enfin2i  10409  fin45  10480  axcc3  10526  engch  10723  hargch  10768  hasheni  14502  pmtrfv  19678  frgpcyg  21891  lbslcic  22159  kardenir  35897  phpreu  38667  ctbnfien  43965