Theorem relen 8944

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

Syntax hints:  ∃wex 1809  Rel wrel 5666  –1-1-onto→wf1o 6535   ≈ cen 8936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-opab 5174  df-xp 5667  df-rel 5668  df-en 8940

This theorem is referenced by:  encv  8947  isfi  8968  enssdomOLD  8970  ener  8994  enfixsn  9070  sbthcl  9083  xpen  9124  pwen  9134  mapfien2  9365  isnum2  9927  inffien  10043  djuen  10149  djuenun  10150  cdainflem  10167  djulepw  10172  infmap2  10196  fin4i  10277  fin4en1  10288  isfin4p1  10294  enfin2i  10300  fin45  10371  axcc3  10417  engch  10608  hargch  10653  hasheni  14380  pmtrfv  19517  frgpcyg  21723  lbslcic  21991  kardenir  35571  phpreu  38275  ctbnfien  43565