Theorem relen 8948

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

Syntax hints:  ∃wex 1806  Rel wrel 5667  –1-1-onto→wf1o 6536   ≈ cen 8940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-opab 5178  df-xp 5668  df-rel 5669  df-en 8944

This theorem is referenced by:  encv  8951  isfi  8972  enssdomOLD  8974  ener  8998  enfixsn  9074  sbthcl  9087  xpen  9128  pwen  9138  mapfien2  9369  isnum2  9931  inffien  10047  djuen  10153  djuenun  10154  cdainflem  10171  djulepw  10176  infmap2  10200  fin4i  10282  fin4en1  10293  isfin4p1  10299  enfin2i  10305  fin45  10376  axcc3  10422  engch  10613  hargch  10658  hasheni  14384  pmtrfv  19522  frgpcyg  21692  lbslcic  21960  kardenir  35504  phpreu  38177  ctbnfien  43471