Theorem relen 8968

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

Syntax hints:  ∃wex 1774  Rel wrel 5683  –1-1-onto→wf1o 6547   ≈ cen 8960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964  df-opab 5211  df-xp 5684  df-rel 5685  df-en 8964

This theorem is referenced by:  encv  8971  isfi  8996  enssdom  8997  ener  9021  en1unielOLD  9053  enfixsn  9105  sbthcl  9119  xpen  9164  pwen  9174  php3OLD  9248  f1finf1oOLD  9296  mapfien2  9432  isnum2  9968  inffien  10086  djuen  10192  djuenun  10193  cdainflem  10210  djulepw  10215  infmap2  10241  fin4i  10321  fin4en1  10332  isfin4p1  10338  enfin2i  10344  fin45  10415  axcc3  10461  engch  10651  hargch  10696  hasheni  14339  pmtrfv  19406  frgpcyg  21506  lbslcic  21774  phpreu  37077  ctbnfien  42238

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »