Theorem relen 8738

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

Syntax hints:  ∃wex 1782  Rel wrel 5594  –1-1-onto→wf1o 6432   ≈ cen 8730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596  df-en 8734

This theorem is referenced by:  encv  8741  isfi  8764  enssdom  8765  ener  8787  en1unielOLD  8819  enfixsn  8868  sbthcl  8882  xpen  8927  pwen  8937  php3OLD  9007  f1finf1o  9046  mapfien2  9168  isnum2  9703  inffien  9819  djuen  9925  djuenun  9926  cdainflem  9943  djulepw  9948  infmap2  9974  fin4i  10054  fin4en1  10065  isfin4p1  10071  enfin2i  10077  fin45  10148  axcc3  10194  engch  10384  hargch  10429  hasheni  14062  pmtrfv  19060  frgpcyg  20781  lbslcic  21048  phpreu  35761  ctbnfien  40640