Theorem relen 8964

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

Syntax hints:  ∃wex 1779  Rel wrel 5659  –1-1-onto→wf1o 6530   ≈ cen 8956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661  df-en 8960

This theorem is referenced by:  encv  8967  isfi  8990  enssdom  8991  ener  9015  enfixsn  9095  sbthcl  9109  xpen  9154  pwen  9164  php3OLD  9233  f1finf1oOLD  9278  mapfien2  9421  isnum2  9959  inffien  10077  djuen  10184  djuenun  10185  cdainflem  10202  djulepw  10207  infmap2  10231  fin4i  10312  fin4en1  10323  isfin4p1  10329  enfin2i  10335  fin45  10406  axcc3  10452  engch  10642  hargch  10687  hasheni  14366  pmtrfv  19433  frgpcyg  21534  lbslcic  21801  phpreu  37628  ctbnfien  42841