Theorem relen 8954

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

This proof depends on syntax axioms:  ∃wex 1812  Rel wrel 5668  –1-1-onto→wf1o 6539   ≈ cen 8946

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-opab 5176  df-xp 5669  df-rel 5670  df-en 8950

This theorem is used by:  encv  8957  isfi  8978  enssdomOLD  8980  ener  9004  enfixsn  9081  sbthcl  9094  xpen  9135  pwen  9145  mapfien2  9376  isnum2  9947  inffien  10063  djuen  10169  djuenun  10170  cdainflem  10187  djulepw  10192  infmap2  10216  fin4i  10297  fin4en1  10308  isfin4p1  10314  enfin2i  10320  fin45  10391  axcc3  10437  engch  10630  hargch  10675  hasheni  14404  pmtrfv  19568  frgpcyg  21775  lbslcic  22043  kardenir  35630  phpreu  38314  ctbnfien  43605