Theorem ssiun2 5004

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 4951	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 252	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3940	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061   ⊆ wss 3902  ∪ ciun 4947

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 3062  df-v 3443  df-ss 3919  df-iun 4949

This theorem is referenced by:  ssiun2s  5005  disjxiun  5096  triun  5220  iunopeqop  5470  ixpf  8862  ixpiunwdom  9499  r1sdom  9690  r1val1  9702  rankuni2b  9769  rankval4  9783  cplem1  9805  domtriomlem  10356  ac6num  10393  iunfo  10453  iundom2g  10454  pwfseqlem3  10575  inar1  10690  tskuni  10698  iunconnlem  23375  ptclsg  23563  ovoliunlem1  25463  limciun  25855  ssiun2sf  32637  iunxpssiun1  32646  djussxp2  32729  suppovss  32762  bnj906  35088  bnj999  35116  bnj1014  35119  bnj1408  35194  rankval4b  35258  rdgssun  37585  cpcolld  44566  iunmapss  45526  ssmapsn  45527  sge0iunmpt  46729  sge0iun  46730  voliunsge0lem  46783  omeiunltfirp  46830