Theorem ssiun2 5070

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3076   ⊆ wss 3976  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-v 3490  df-ss 3993  df-iun 5017

This theorem is referenced by:  ssiun2s  5071  disjxiun  5163  triun  5298  iunopeqop  5540  ixpf  8978  ixpiunwdom  9659  r1sdom  9843  r1val1  9855  rankuni2b  9922  rankval4  9936  cplem1  9958  domtriomlem  10511  ac6num  10548  iunfo  10608  iundom2g  10609  pwfseqlem3  10729  inar1  10844  tskuni  10852  iunconnlem  23456  ptclsg  23644  ovoliunlem1  25556  limciun  25949  ssiun2sf  32582  djussxp2  32666  suppovss  32697  bnj906  34906  bnj999  34934  bnj1014  34937  bnj1408  35012  rdgssun  37344  cpcolld  44227  iunmapss  45122  ssmapsn  45123  sge0iunmpt  46339  sge0iun  46340  voliunsge0lem  46393  omeiunltfirp  46440