Theorem ssiun2 4980

Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
ssiun2	⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Proof of Theorem ssiun2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rspe 3231	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 414	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4928	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 254	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3923	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2121  ∃wrex 3065   ⊆ wss 3885  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rex 3066  df-v 3435  df-ss 3902  df-iun 4926

This theorem is referenced by:  ssiun2s  4981  disjxiun  5072  triun  5197  iunopeqop  5465  iunopeqopOLD  5466  ixpf  8862  ixpiunwdom  9499  r1sdom  9693  r1val1  9705  rankuni2b  9772  rankval4  9786  cplem1  9808  domtriomlem  10359  ac6num  10396  iunfo  10456  iundom2g  10457  pwfseqlem3  10578  inar1  10693  tskuni  10701  iunconnlem  23414  ptclsg  23602  ovoliunlem1  25491  limciun  25883  ssiun2sf  32652  iunxpssiun1  32661  djussxp2  32744  suppovss  32777  bnj906  35127  bnj999  35155  bnj1014  35158  bnj1408  35233  rankval4b  35296  rdgssun  37755  cpcolld  44717  iunmapss  45674  ssmapsn  45675  sge0iunmpt  46875  sge0iun  46876  voliunsge0lem  46929  omeiunltfirp  46976