![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > intex | Structured version Visualization version Unicode version |
Description: The intersection of a nonempty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.) |
Ref | Expression |
---|---|
intex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0 3753 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | intss1 4263 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | vex 3060 |
. . . . . 6
![]() ![]() ![]() ![]() | |
4 | 3 | ssex 4561 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | syl 17 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | exlimiv 1787 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 6 | sylbi 200 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | vprc 4555 |
. . . 4
![]() ![]() ![]() ![]() ![]() | |
9 | inteq 4251 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | int0 4262 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | syl6eq 2512 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | eleq1d 2524 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 8, 12 | mtbiri 309 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | necon2ai 2665 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 7, 14 | impbii 192 |
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 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-v 3059 df-dif 3419 df-in 3423 df-ss 3430 df-nul 3744 df-int 4249 |
This theorem is referenced by: intnex 4574 intexab 4575 iinexg 4577 onint0 6650 onintrab 6655 onmindif2 6666 fival 7952 elfi2 7954 elfir 7955 dffi2 7963 elfiun 7970 fifo 7972 tz9.1c 8240 tz9.12lem1 8284 tz9.12lem3 8286 rankf 8291 cardf2 8403 cardval3 8412 cardid2 8413 cardcf 8708 cflim2 8719 intwun 9186 wuncval 9193 inttsk 9225 intgru 9265 gruina 9269 dfrtrcl2 13174 mremre 15559 mrcval 15565 asplss 18602 aspsubrg 18604 toponmre 20158 subbascn 20319 insiga 29008 sigagenval 29011 sigagensiga 29012 dmsigagen 29015 dfon2lem8 30485 dfon2lem9 30486 igenval 32339 pclvalN 33500 elrfi 35581 ismrcd1 35585 mzpval 35619 dmmzp 35620 salgenval 38220 intsal 38227 |
Copyright terms: Public domain | W3C validator |