Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > relen | Structured version Visualization version GIF version |
Description: Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.) |
Ref | Expression |
---|---|
relen | ⊢ Rel ≈ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-en 8734 | . 2 ⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} | |
2 | 1 | relopabiv 5730 | 1 ⊢ Rel ≈ |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1782 Rel wrel 5594 –1-1-onto→wf1o 6432 ≈ cen 8730 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-in 3894 df-ss 3904 df-opab 5137 df-xp 5595 df-rel 5596 df-en 8734 |
This theorem is referenced by: encv 8741 isfi 8764 enssdom 8765 ener 8787 en1unielOLD 8819 enfixsn 8868 sbthcl 8882 xpen 8927 pwen 8937 php3OLD 9007 f1finf1o 9046 mapfien2 9168 isnum2 9703 inffien 9819 djuen 9925 djuenun 9926 cdainflem 9943 djulepw 9948 infmap2 9974 fin4i 10054 fin4en1 10065 isfin4p1 10071 enfin2i 10077 fin45 10148 axcc3 10194 engch 10384 hargch 10429 hasheni 14062 pmtrfv 19060 frgpcyg 20781 lbslcic 21048 phpreu 35761 ctbnfien 40640 |
Copyright terms: Public domain | W3C validator |