Theorem relen 8696

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

Syntax hints:  ∃wex 1783  Rel wrel 5585  –1-1-onto→wf1o 6417   ≈ cen 8688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587  df-en 8692

This theorem is referenced by:  encv  8699  isfi  8719  enssdom  8720  ener  8742  en1unielOLD  8773  enfixsn  8821  sbthcl  8835  xpen  8876  pwen  8886  php3  8899  f1finf1o  8975  mapfien2  9098  isnum2  9634  inffien  9750  djuen  9856  djuenun  9857  cdainflem  9874  djulepw  9879  infmap2  9905  fin4i  9985  fin4en1  9996  isfin4p1  10002  enfin2i  10008  fin45  10079  axcc3  10125  engch  10315  hargch  10360  hasheni  13990  pmtrfv  18975  frgpcyg  20693  lbslcic  20958  phpreu  35688  ctbnfien  40556