Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssiun2s | Structured version Visualization version GIF version |
Description: Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.) |
Ref | Expression |
---|---|
ssiun2s.1 | ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
ssiun2s | ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2908 | . 2 ⊢ Ⅎ𝑥𝐶 | |
2 | nfcv 2908 | . . 3 ⊢ Ⅎ𝑥𝐷 | |
3 | nfiu1 4959 | . . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 | |
4 | 2, 3 | nfss 3914 | . 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | ssiun2s.1 | . . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) | |
6 | 5 | sseq1d 3953 | . 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)) |
7 | ssiun2 4978 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | |
8 | 1, 4, 6, 7 | vtoclgaf 3513 | 1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 ⊆ wss 3888 ∪ ciun 4925 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ral 3070 df-rex 3071 df-v 3435 df-in 3895 df-ss 3905 df-iun 4927 |
This theorem is referenced by: fviunfun 7796 onfununi 8181 oaordi 8386 omordi 8406 dffi3 9199 alephordi 9839 domtriomlem 10207 pwxpndom2 10430 wunex2 10503 imasaddvallem 17249 imasvscaval 17258 iundisj2 24722 voliunlem1 24723 volsup 24729 iundisj2fi 31127 bnj906 32919 bnj1137 32984 bnj1408 33025 cvmliftlem10 33265 cvmliftlem13 33267 sstotbnd2 35941 mapdrvallem3 39667 fvmptiunrelexplb0d 41299 fvmptiunrelexplb1d 41301 corclrcl 41322 trclrelexplem 41326 corcltrcl 41354 cotrclrcl 41357 iunincfi 42651 iundjiunlem 44004 meaiuninc3v 44029 caratheodorylem1 44071 ovnhoilem1 44146 |
Copyright terms: Public domain | W3C validator |