![]() |
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 3230 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
2 | 1 | ex 413 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
3 | eliun 4956 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
4 | 2, 3 | syl6ibr 251 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)) |
5 | 4 | ssrdv 3948 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∃wrex 3071 ⊆ wss 3908 ∪ ciun 4952 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rex 3072 df-v 3445 df-in 3915 df-ss 3925 df-iun 4954 |
This theorem is referenced by: ssiun2s 5006 disjxiun 5100 triun 5235 iunopeqop 5476 ixpf 8816 ixpiunwdom 9484 r1sdom 9668 r1val1 9680 rankuni2b 9747 rankval4 9761 cplem1 9783 domtriomlem 10336 ac6num 10373 iunfo 10433 iundom2g 10434 pwfseqlem3 10554 inar1 10669 tskuni 10677 iunconnlem 22724 ptclsg 22912 ovoliunlem1 24812 limciun 25204 ssiun2sf 31323 djussxp2 31409 suppovss 31441 bnj906 33370 bnj999 33398 bnj1014 33401 bnj1408 33476 rdgssun 35781 cpcolld 42443 iunmapss 43335 ssmapsn 43336 sge0iunmpt 44554 sge0iun 44555 voliunsge0lem 44608 omeiunltfirp 44655 |
Copyright terms: Public domain | W3C validator |