Theorem ssiun2 5011

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

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

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 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  ssiun2s  5012  disjxiun  5104  triun  5229  iunopeqop  5481  ixpf  8893  ixpiunwdom  9543  r1sdom  9727  r1val1  9739  rankuni2b  9806  rankval4  9820  cplem1  9842  domtriomlem  10395  ac6num  10432  iunfo  10492  iundom2g  10493  pwfseqlem3  10613  inar1  10728  tskuni  10736  iunconnlem  23314  ptclsg  23502  ovoliunlem1  25403  limciun  25795  ssiun2sf  32488  iunxpssiun1  32497  djussxp2  32572  suppovss  32604  bnj906  34920  bnj999  34948  bnj1014  34951  bnj1408  35026  rdgssun  37366  cpcolld  44247  iunmapss  45209  ssmapsn  45210  sge0iunmpt  46416  sge0iun  46417  voliunsge0lem  46470  omeiunltfirp  46517