Theorem ssiun2 5051

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 3246	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 412	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4999	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 252	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 4000	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3067   ⊆ wss 3962  ∪ ciun 4995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-v 3479  df-ss 3979  df-iun 4997

This theorem is referenced by:  ssiun2s  5052  disjxiun  5144  triun  5279  iunopeqop  5530  ixpf  8958  ixpiunwdom  9627  r1sdom  9811  r1val1  9823  rankuni2b  9890  rankval4  9904  cplem1  9926  domtriomlem  10479  ac6num  10516  iunfo  10576  iundom2g  10577  pwfseqlem3  10697  inar1  10812  tskuni  10820  iunconnlem  23450  ptclsg  23638  ovoliunlem1  25550  limciun  25943  ssiun2sf  32579  djussxp2  32664  suppovss  32695  bnj906  34922  bnj999  34950  bnj1014  34953  bnj1408  35028  rdgssun  37360  cpcolld  44253  iunmapss  45157  ssmapsn  45158  sge0iunmpt  46373  sge0iun  46374  voliunsge0lem  46427  omeiunltfirp  46474