Theorem ssiun2 5023

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3060   ⊆ wss 3926  ∪ ciun 4967

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461  df-ss 3943  df-iun 4969

This theorem is referenced by:  ssiun2s  5024  disjxiun  5116  triun  5244  iunopeqop  5496  ixpf  8932  ixpiunwdom  9602  r1sdom  9786  r1val1  9798  rankuni2b  9865  rankval4  9879  cplem1  9901  domtriomlem  10454  ac6num  10491  iunfo  10551  iundom2g  10552  pwfseqlem3  10672  inar1  10787  tskuni  10795  iunconnlem  23363  ptclsg  23551  ovoliunlem1  25453  limciun  25845  ssiun2sf  32486  iunxpssiun1  32495  djussxp2  32572  suppovss  32604  bnj906  34907  bnj999  34935  bnj1014  34938  bnj1408  35013  rdgssun  37342  cpcolld  44230  iunmapss  45187  ssmapsn  45188  sge0iunmpt  46395  sge0iun  46396  voliunsge0lem  46449  omeiunltfirp  46496