![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iunexg | Structured version Visualization version Unicode version |
Description: The existence of an
indexed union. ![]() ![]() |
Ref | Expression |
---|---|
iunexg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfiun2g 4280 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 472 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | abrexexg 6756 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | uniexg 6576 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl 17 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | adantr 471 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 6 | eqeltrd 2530 |
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 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-8 1893 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-rep 4487 ax-sep 4497 ax-nul 4506 ax-pr 4612 ax-un 6571 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3015 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-sn 3937 df-pr 3939 df-op 3943 df-uni 4169 df-iun 4250 df-br 4375 df-opab 4434 df-mpt 4435 df-id 4727 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-iota 5525 df-fun 5563 df-fn 5564 df-f 5565 df-f1 5566 df-fo 5567 df-f1o 5568 df-fv 5569 |
This theorem is referenced by: abrexex2g 6758 opabex3d 6759 opabex3 6760 iunex 6761 xpexgALT 6774 mpt2exxg 6855 ixpexg 7533 ixpssmapg 7539 iundom 8954 iunctb 8986 cshwsex 15082 imasplusg 15429 imasmulr 15430 imasvsca 15432 imasip 15433 gsum2d2 17617 gsumcom2 17618 dprd2da 17686 ptcls 20642 ptcmplem2 21079 elpwiuncl 28167 aciunf1lem 28272 esum2dlem 28920 esum2d 28921 esumiun 28922 omssubadd 29134 omssubaddOLD 29138 eulerpartlemgs2 29219 bnj535 29707 bnj546 29713 bnj893 29745 bnj1136 29812 bnj1413 29850 trpredtr 30477 trpredmintr 30478 trpredrec 30485 eliunov2 36273 fvmptiunrelexplb0d 36278 fvmptiunrelexplb1d 36280 iunrelexp0 36296 unirnmapsn 37508 iunmapss 37509 ssmapsn 37510 iunmapsn 37511 sge0iunmptlemfi 38314 sge0iunmpt 38319 mpt2exxg2 40444 |
Copyright terms: Public domain | W3C validator |