Theorem relen 8978

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

This proof depends on syntax axioms:  ∃wex 1812  Rel wrel 5656  –1-1-onto→wf1o 6537   ≈ cen 8970

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658  df-en 8974

This theorem is used by:  encv  8981  isfi  9002  enssdomOLD  9004  ener  9028  enfixsn  9105  sbthcl  9118  xpen  9159  pwen  9169  mapfien2  9401  isnum2  10026  inffien  10142  djuen  10248  djuenun  10249  cdainflem  10266  djulepw  10271  infmap2  10295  fin4i  10376  fin4en1  10387  isfin4p1  10393  enfin2i  10399  fin45  10470  axcc3  10516  engch  10713  hargch  10758  hasheni  14492  pmtrfv  19666  frgpcyg  21879  lbslcic  22147  kardenir  35826  phpreu  38527  ctbnfien  43824