Theorem relen 8497

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

Syntax hints:  ∃wex 1781  Rel wrel 5524  –1-1-onto→wf1o 6323   ≈ cen 8489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-xp 5525  df-rel 5526  df-en 8493

This theorem is referenced by:  encv  8500  isfi  8516  enssdom  8517  ener  8539  en1uniel  8564  enfixsn  8609  sbthcl  8623  xpen  8664  pwen  8674  php3  8687  f1finf1o  8729  mapfien2  8856  isnum2  9358  inffien  9474  djuen  9580  djuenun  9581  cdainflem  9598  djulepw  9603  infmap2  9629  fin4i  9709  fin4en1  9720  isfin4p1  9726  enfin2i  9732  fin45  9803  axcc3  9849  engch  10039  hargch  10084  hasheni  13704  pmtrfv  18572  frgpcyg  20265  lbslcic  20530  phpreu  35041  ctbnfien  39759