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 2899 | . 2 ⊢ Ⅎ𝑥𝐶 | |
2 | nfcv 2899 | . . 3 ⊢ Ⅎ𝑥𝐷 | |
3 | nfiu1 4915 | . . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 | |
4 | 2, 3 | nfss 3869 | . 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | ssiun2s.1 | . . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) | |
6 | 5 | sseq1d 3908 | . 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)) |
7 | ssiun2 4933 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | |
8 | 1, 4, 6, 7 | vtoclgaf 3477 | 1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ⊆ wss 3843 ∪ ciun 4881 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-v 3400 df-in 3850 df-ss 3860 df-iun 4883 |
This theorem is referenced by: fviunfun 7671 onfununi 8007 oaordi 8203 omordi 8223 dffi3 8968 alephordi 9574 domtriomlem 9942 pwxpndom2 10165 wunex2 10238 imasaddvallem 16905 imasvscaval 16914 iundisj2 24301 voliunlem1 24302 volsup 24308 iundisj2fi 30693 bnj906 32481 bnj1137 32546 bnj1408 32587 cvmliftlem10 32827 cvmliftlem13 32829 sstotbnd2 35555 mapdrvallem3 39283 fvmptiunrelexplb0d 40838 fvmptiunrelexplb1d 40840 corclrcl 40861 trclrelexplem 40865 corcltrcl 40893 cotrclrcl 40896 iunincfi 42182 iundjiunlem 43539 meaiuninc3v 43564 caratheodorylem1 43606 ovnhoilem1 43681 |
Copyright terms: Public domain | W3C validator |