![]() |
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 2903 | . 2 ⊢ Ⅎ𝑥𝐶 | |
2 | nfcv 2903 | . . 3 ⊢ Ⅎ𝑥𝐷 | |
3 | nfiu1 5032 | . . 3 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 | |
4 | 2, 3 | nfss 3988 | . 2 ⊢ Ⅎ𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | ssiun2s.1 | . . 3 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) | |
6 | 5 | sseq1d 4027 | . 2 ⊢ (𝑥 = 𝐶 → (𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)) |
7 | ssiun2 5052 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) | |
8 | 1, 4, 6, 7 | vtoclgaf 3576 | 1 ⊢ (𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 ⊆ wss 3963 ∪ ciun 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ral 3060 df-rex 3069 df-v 3480 df-ss 3980 df-iun 4998 |
This theorem is referenced by: fviunfun 7968 onfununi 8380 oaordi 8583 omordi 8603 dffi3 9469 alephordi 10112 domtriomlem 10480 pwxpndom2 10703 wunex2 10776 imasaddvallem 17576 imasvscaval 17585 iundisj2 25598 voliunlem1 25599 volsup 25605 iundisj2fi 32805 constr01 33747 bnj906 34923 bnj1137 34988 bnj1408 35029 cvmliftlem10 35279 cvmliftlem13 35281 sstotbnd2 37761 mapdrvallem3 41629 onsucunifi 43360 fvmptiunrelexplb0d 43674 fvmptiunrelexplb1d 43676 corclrcl 43697 trclrelexplem 43701 corcltrcl 43729 cotrclrcl 43732 iunincfi 45034 iundjiunlem 46415 meaiuninc3v 46440 caratheodorylem1 46482 ovnhoilem1 46557 |
Copyright terms: Public domain | W3C validator |