![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssiun2 | Structured version Visualization version GIF version |
Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
ssiun2 | ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspe 3247 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
2 | 1 | ex 414 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
3 | eliun 5002 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
4 | 2, 3 | imbitrrdi 251 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)) |
5 | 4 | ssrdv 3989 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ∃wrex 3071 ⊆ wss 3949 ∪ ciun 4998 |
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-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rex 3072 df-v 3477 df-in 3956 df-ss 3966 df-iun 5000 |
This theorem is referenced by: ssiun2s 5052 disjxiun 5146 triun 5281 iunopeqop 5522 ixpf 8914 ixpiunwdom 9585 r1sdom 9769 r1val1 9781 rankuni2b 9848 rankval4 9862 cplem1 9884 domtriomlem 10437 ac6num 10474 iunfo 10534 iundom2g 10535 pwfseqlem3 10655 inar1 10770 tskuni 10778 iunconnlem 22931 ptclsg 23119 ovoliunlem1 25019 limciun 25411 ssiun2sf 31791 djussxp2 31873 suppovss 31906 bnj906 33941 bnj999 33969 bnj1014 33972 bnj1408 34047 rdgssun 36259 cpcolld 43017 iunmapss 43914 ssmapsn 43915 sge0iunmpt 45134 sge0iun 45135 voliunsge0lem 45188 omeiunltfirp 45235 |
Copyright terms: Public domain | W3C validator |