![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bren | Structured version Visualization version Unicode version |
Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) |
Ref | Expression |
---|---|
bren |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | encv 7603 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | f1ofn 5838 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | fndm 5697 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | vex 3060 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
5 | 4 | dmex 6753 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | syl6eqelr 2549 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 6 | syl 17 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | f1ofo 5844 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | forn 5819 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 8, 9 | syl 17 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 4 | rnex 6754 |
. . . . 5
![]() ![]() ![]() ![]() ![]() |
12 | 10, 11 | syl6eqelr 2549 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 7, 12 | jca 539 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | exlimiv 1787 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | f1oeq2 5829 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 15 | exbidv 1779 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | f1oeq3 5830 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | 17 | exbidv 1779 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | df-en 7596 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
20 | 16, 18, 19 | brabg 4734 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 1, 14, 20 | pm5.21nii 359 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pr 4653 ax-un 6610 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-xp 4859 df-rel 4860 df-cnv 4861 df-dm 4863 df-rn 4864 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-en 7596 |
This theorem is referenced by: domen 7608 f1oen3g 7611 ener 7642 en0 7658 ensn1 7659 en1 7662 unen 7678 enfixsn 7707 canth2 7751 mapen 7762 ssenen 7772 phplem4 7780 php3 7784 isinf 7811 ssfi 7818 domunfican 7870 fiint 7874 mapfien2 7948 unxpwdom2 8129 isinffi 8452 infxpenc2 8479 fseqen 8484 dfac8b 8488 infpwfien 8519 dfac12r 8602 infmap2 8674 cff1 8714 infpssr 8764 fin4en1 8765 enfin2i 8777 enfin1ai 8840 axcc3 8894 axcclem 8913 numth 8928 ttukey2g 8972 canthnum 9100 canthwe 9102 canthp1 9105 pwfseq 9115 tskuni 9234 gruen 9263 hasheqf1o 12564 hashfacen 12650 fz1f1o 13825 ruc 14344 cnso 14348 eulerth 14780 ablfaclem3 17769 lbslcic 19448 uvcendim 19454 indishmph 20862 ufldom 21026 ovolctb 22492 ovoliunlem3 22506 iunmbl2 22559 dyadmbl 22607 vitali 22620 nbusgrafi 25225 cusgrafilem3 25258 wlknwwlknen 25492 padct 28356 f1ocnt 28425 volmeas 29103 eulerpart 29264 derangenlem 29943 mblfinlem1 32022 eldioph2lem1 35647 isnumbasgrplem1 36005 nnf1oxpnn 37510 cusgrfilem3 39568 |
Copyright terms: Public domain | W3C validator |