Theorem ssiun2 5005

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062   ⊆ wss 3903  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  ssiun2s  5006  disjxiun  5097  triun  5221  iunopeqop  5479  ixpf  8872  ixpiunwdom  9509  r1sdom  9700  r1val1  9712  rankuni2b  9779  rankval4  9793  cplem1  9815  domtriomlem  10366  ac6num  10403  iunfo  10463  iundom2g  10464  pwfseqlem3  10585  inar1  10700  tskuni  10708  iunconnlem  23388  ptclsg  23576  ovoliunlem1  25476  limciun  25868  ssiun2sf  32652  iunxpssiun1  32661  djussxp2  32744  suppovss  32777  bnj906  35112  bnj999  35140  bnj1014  35143  bnj1408  35218  rankval4b  35283  rdgssun  37660  cpcolld  44643  iunmapss  45602  ssmapsn  45603  sge0iunmpt  46805  sge0iun  46806  voliunsge0lem  46859  omeiunltfirp  46906