Theorem ssiun2 4979

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3059   ⊆ wss 3885  ∪ ciun 4923

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2184  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rex 3060  df-v 3429  df-ss 3902  df-iun 4925

This theorem is referenced by:  ssiun2s  4980  disjxiun  5071  triun  5196  iunopeqop  5464  iunopeqopOLD  5465  ixpf  8857  ixpiunwdom  9494  r1sdom  9687  r1val1  9699  rankuni2b  9766  rankval4  9780  cplem1  9802  domtriomlem  10353  ac6num  10390  iunfo  10450  iundom2g  10451  pwfseqlem3  10572  inar1  10687  tskuni  10695  iunconnlem  23380  ptclsg  23568  ovoliunlem1  25457  limciun  25849  ssiun2sf  32617  iunxpssiun1  32626  djussxp2  32709  suppovss  32742  bnj906  35060  bnj999  35088  bnj1014  35091  bnj1408  35166  rankval4b  35231  rdgssun  37682  cpcolld  44673  iunmapss  45632  ssmapsn  45633  sge0iunmpt  46834  sge0iun  46835  voliunsge0lem  46888  omeiunltfirp  46935