Theorem relen 9008

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

Syntax hints:  ∃wex 1777  Rel wrel 5705  –1-1-onto→wf1o 6572   ≈ cen 9000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707  df-en 9004

This theorem is referenced by:  encv  9011  isfi  9036  enssdom  9037  ener  9061  en1unielOLD  9094  enfixsn  9147  sbthcl  9161  xpen  9206  pwen  9216  php3OLD  9287  f1finf1oOLD  9334  mapfien2  9478  isnum2  10014  inffien  10132  djuen  10239  djuenun  10240  cdainflem  10257  djulepw  10262  infmap2  10286  fin4i  10367  fin4en1  10378  isfin4p1  10384  enfin2i  10390  fin45  10461  axcc3  10507  engch  10697  hargch  10742  hasheni  14397  pmtrfv  19494  frgpcyg  21615  lbslcic  21884  phpreu  37564  ctbnfien  42774