Theorem ssiun2 5002

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3059   ⊆ wss 3900  ∪ ciun 4945

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 2183  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rex 3060  df-v 3441  df-ss 3917  df-iun 4947

This theorem is referenced by:  ssiun2s  5003  disjxiun  5094  triun  5218  iunopeqop  5468  ixpf  8860  ixpiunwdom  9497  r1sdom  9688  r1val1  9700  rankuni2b  9767  rankval4  9781  cplem1  9803  domtriomlem  10354  ac6num  10391  iunfo  10451  iundom2g  10452  pwfseqlem3  10573  inar1  10688  tskuni  10696  iunconnlem  23373  ptclsg  23561  ovoliunlem1  25461  limciun  25853  ssiun2sf  32614  iunxpssiun1  32623  djussxp2  32706  suppovss  32739  bnj906  35065  bnj999  35093  bnj1014  35096  bnj1408  35171  rankval4b  35235  rdgssun  37552  cpcolld  44536  iunmapss  45496  ssmapsn  45497  sge0iunmpt  46699  sge0iun  46700  voliunsge0lem  46753  omeiunltfirp  46800