| 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 3249 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
| 2 | 1 | ex 412 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
| 3 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
| 4 | 2, 3 | imbitrrdi 252 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)) |
| 5 | 4 | ssrdv 3989 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∃wrex 3070 ⊆ wss 3951 ∪ ciun 4991 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-v 3482 df-ss 3968 df-iun 4993 |
| This theorem is referenced by: ssiun2s 5048 disjxiun 5140 triun 5274 iunopeqop 5526 ixpf 8960 ixpiunwdom 9630 r1sdom 9814 r1val1 9826 rankuni2b 9893 rankval4 9907 cplem1 9929 domtriomlem 10482 ac6num 10519 iunfo 10579 iundom2g 10580 pwfseqlem3 10700 inar1 10815 tskuni 10823 iunconnlem 23435 ptclsg 23623 ovoliunlem1 25537 limciun 25929 ssiun2sf 32572 iunxpssiun1 32581 djussxp2 32658 suppovss 32690 bnj906 34944 bnj999 34972 bnj1014 34975 bnj1408 35050 rdgssun 37379 cpcolld 44277 iunmapss 45220 ssmapsn 45221 sge0iunmpt 46433 sge0iun 46434 voliunsge0lem 46487 omeiunltfirp 46534 |
| Copyright terms: Public domain | W3C validator |