Theorem ssiun2 5006

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 4955	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 252	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3949	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053   ⊆ wss 3911  ∪ ciun 4951

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  ssiun2s  5007  disjxiun  5099  triun  5224  iunopeqop  5476  ixpf  8870  ixpiunwdom  9519  r1sdom  9703  r1val1  9715  rankuni2b  9782  rankval4  9796  cplem1  9818  domtriomlem  10371  ac6num  10408  iunfo  10468  iundom2g  10469  pwfseqlem3  10589  inar1  10704  tskuni  10712  iunconnlem  23347  ptclsg  23535  ovoliunlem1  25436  limciun  25828  ssiun2sf  32538  iunxpssiun1  32547  djussxp2  32622  suppovss  32654  bnj906  34913  bnj999  34941  bnj1014  34944  bnj1408  35019  rdgssun  37359  cpcolld  44240  iunmapss  45202  ssmapsn  45203  sge0iunmpt  46409  sge0iun  46410  voliunsge0lem  46463  omeiunltfirp  46510