Theorem relen 8886

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

Syntax hints:  ∃wex 1780  Rel wrel 5627  –1-1-onto→wf1o 6489   ≈ cen 8878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-opab 5159  df-xp 5628  df-rel 5629  df-en 8882

This theorem is referenced by:  encv  8889  isfi  8910  enssdomOLD  8912  ener  8936  enfixsn  9012  sbthcl  9025  xpen  9066  pwen  9076  mapfien2  9310  isnum2  9855  inffien  9971  djuen  10078  djuenun  10079  cdainflem  10096  djulepw  10101  infmap2  10125  fin4i  10206  fin4en1  10217  isfin4p1  10223  enfin2i  10229  fin45  10300  axcc3  10346  engch  10537  hargch  10582  hasheni  14269  pmtrfv  19379  frgpcyg  21526  lbslcic  21794  phpreu  37744  ctbnfien  43002