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 2751 | . 2 ⊢ Ⅎ𝑥𝐶 | |
2 | nfcv 2751 | . . 3 ⊢ Ⅎ𝑥𝐷 | |
3 | nfiu1 4486 | . . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 | |
4 | 2, 3 | nfss 3561 | . 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | ssiun2s.1 | . . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) | |
6 | 5 | sseq1d 3595 | . 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)) |
7 | ssiun2 4499 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | |
8 | 1, 4, 6, 7 | vtoclgaf 3244 | 1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ⊆ wss 3540 ∪ ciun 4455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-v 3175 df-in 3547 df-ss 3554 df-iun 4457 |
This theorem is referenced by: onfununi 7325 oaordi 7513 omordi 7533 dffi3 8220 alephordi 8780 domtriomlem 9147 pwxpndom2 9366 wunex2 9439 imasaddvallem 16012 imasvscaval 16021 iundisj2 23124 voliunlem1 23125 volsup 23131 iundisj2fi 28943 bnj906 30254 bnj1137 30317 bnj1408 30358 cvmliftlem10 30530 cvmliftlem13 30532 sstotbnd2 32743 mapdrvallem3 35953 fvmptiunrelexplb0d 36995 fvmptiunrelexplb1d 36997 corclrcl 37018 trclrelexplem 37022 corcltrcl 37050 cotrclrcl 37053 iunincfi 38300 iundjiunlem 39352 caratheodorylem1 39416 ovnhoilem1 39491 |
Copyright terms: Public domain | W3C validator |