![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfiu1 | Structured version Visualization version Unicode version |
Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) |
Ref | Expression |
---|---|
nfiu1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun 4271 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfre1 2846 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | nfab 2616 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | nfcxfr 2610 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-rex 2762 df-iun 4271 |
This theorem is referenced by: ssiun2s 4313 disjxiun 4392 triun 4503 eliunxp 4977 opeliunxp2 4978 opeliunxp2f 6975 ixpf 7562 ixpiunwdom 8124 r1val1 8275 rankuni2b 8342 rankval4 8356 cplem2 8379 ac6num 8927 iunfo 8982 iundom2g 8983 inar1 9218 tskuni 9226 gsum2d2lem 17683 gsum2d2 17684 gsumcom2 17685 iuncon 20520 ptclsg 20707 cnextfvval 21158 ssiun2sf 28252 aciunf1lem 28339 esum2dlem 28987 esum2d 28988 esumiun 28989 sigapildsys 29058 bnj958 29823 bnj1000 29824 bnj981 29833 bnj1398 29915 bnj1408 29917 iunconlem2 37395 iunmapss 37568 iunmapsn 37570 fsumiunss 37750 dvnprodlem1 37918 dvnprodlem2 37919 sge0iunmptlemfi 38369 sge0iunmptlemre 38371 sge0iunmpt 38374 iundjiun 38414 voliunsge0lem 38426 caratheodorylem2 38467 iunopeqop 39151 eliunxp2 40623 |
Copyright terms: Public domain | W3C validator |