![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbviunv | Structured version Visualization version Unicode version |
Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 15-Sep-2003.) |
Ref | Expression |
---|---|
cbviunv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cbviunv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2603 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2603 |
. 2
![]() ![]() ![]() ![]() | |
3 | cbviunv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | cbviun 4329 |
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-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
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-ral 2754 df-rex 2755 df-iun 4294 |
This theorem is referenced by: iunxdif2 4340 otiunsndisj 4721 onfununi 7086 oelim2 7322 marypha2lem2 7976 trcl 8238 r1om 8700 fictb 8701 cfsmolem 8726 cfsmo 8727 domtriomlem 8898 domtriom 8899 pwfseq 9115 wunex2 9189 wuncval2 9198 fsuppmapnn0fiubex 12236 ackbijnn 13935 efgs1b 17435 ablfaclem3 17769 ptbasfi 20645 bcth3 22348 itg1climres 22721 2spotiundisj 25839 hashunif 28428 bnj601 29780 cvmliftlem15 30070 trpredlem1 30517 trpredtr 30520 trpredmintr 30521 trpredrec 30528 neibastop2 31066 filnetlem4 31086 sstotbnd2 32151 heiborlem3 32190 heibor 32198 lcfr 35198 mapdrval 35260 corclrcl 36344 trclrelexplem 36348 dftrcl3 36357 cotrcltrcl 36362 dfrtrcl3 36370 corcltrcl 36376 cotrclrcl 36379 carageniuncllem2 38381 caratheodorylem1 38385 caratheodorylem2 38386 caratheodory 38387 ovnsubadd 38432 hoidmv1le 38454 hoidmvle 38460 ovnhoilem2 38462 hspmbl 38489 otiunsndisjX 39046 |
Copyright terms: Public domain | W3C validator |