Theorem relen 8892

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

Syntax hints:  ∃wex 1781  Rel wrel 5630  –1-1-onto→wf1o 6492   ≈ cen 8884

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-opab 5149  df-xp 5631  df-rel 5632  df-en 8888

This theorem is referenced by:  encv  8895  isfi  8916  enssdomOLD  8918  ener  8942  enfixsn  9018  sbthcl  9031  xpen  9072  pwen  9082  mapfien2  9316  isnum2  9863  inffien  9979  djuen  10086  djuenun  10087  cdainflem  10104  djulepw  10109  infmap2  10133  fin4i  10214  fin4en1  10225  isfin4p1  10231  enfin2i  10237  fin45  10308  axcc3  10354  engch  10545  hargch  10590  hasheni  14304  pmtrfv  19421  frgpcyg  21566  lbslcic  21834  phpreu  37942  ctbnfien  43267