Theorem ssiun2 4984

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 3229	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 414	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4935	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	syl6ibr 252	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3932	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2104  ∃wrex 3071   ⊆ wss 3892  ∪ ciun 4931

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3072  df-v 3439  df-in 3899  df-ss 3909  df-iun 4933

This theorem is referenced by:  ssiun2s  4985  disjxiun  5078  triun  5213  iunopeqop  5448  ixpf  8739  ixpiunwdom  9393  r1sdom  9576  r1val1  9588  rankuni2b  9655  rankval4  9669  cplem1  9691  domtriomlem  10244  ac6num  10281  iunfo  10341  iundom2g  10342  pwfseqlem3  10462  inar1  10577  tskuni  10585  iunconnlem  22623  ptclsg  22811  ovoliunlem1  24711  limciun  25103  ssiun2sf  30944  djussxp2  31030  suppovss  31062  bnj906  32955  bnj999  32983  bnj1014  32986  bnj1408  33061  rdgssun  35593  cpcolld  41914  iunmapss  42799  ssmapsn  42800  sge0iunmpt  44006  sge0iun  44007  voliunsge0lem  44060  omeiunltfirp  44107