Theorem relen 4363

Description: Equinumerosity is a relation.

Assertion

Ref	Expression
relen	|- Rel ~~

Proof of Theorem relen

Step	Hyp	Ref	Expression
1		relopab 3262	. 2 |- Rel {<.x, y>. | E.f f:x-1-1-onto->y}
2		df-en 4360	. . 3 |- ~~ = {<.x, y>. | E.f f:x-1-1-onto->y}
3	2	releqi 3240	. 2 |- (Rel ~~ <-> Rel {<.x, y>. | E.f f:x-1-1-onto->y})
4	1, 3	mpbir 190	1 |- Rel ~~

Syntax hints:  E.wex 979  {copab 2662  Rel wrel 3171  -1-1-onto->wf1o 3177   ~~ cen 4357

This theorem is referenced by:  breng 4366  enssdom 4373  ensymg 4401  entrt 4404  unen 4423  sbthcl 4448  sdomen2 4471  pwen 4492  php3 4504  domfi 4525  unifi 4541  fodomfi 4549  fodomfib 4550  iunfi 4552  pwfi 4554  card1 4816

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-pr 2775

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-op 2413  df-opab 2663  df-xp 3180  df-rel 3181  df-en 4360

Copyright terms: Public domain