Theorem ssiun2 5010

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 3254	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 418	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4958	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 255	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3940	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3088   ⊆ wss 3902  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3455  df-ss 3919  df-iun 4956

This theorem is used by:  ssiun2s  5011  disjxiun  5104  triun  5231  iunopeqop  5502  iunopeqopOLD  5503  ixpf  8930  ixpiunwdom  9565  r1sdom  9759  r1val1  9771  rankuni2b  9838  rankval4  9852  cplem1  9892  cplem1OLD  9893  domtriomlem  10447  ac6num  10484  iunfo  10550  iundom2g  10551  pwfseqlem3  10672  inar1  10787  tskuni  10795  iunconnlem  23653  ptclsg  23842  ovoliunlem1  25731  limciun  26123  ssiun2sf  33019  iunxpssiun1  33028  djussxp2  33108  suppovss  33140  bnj906  35426  bnj999  35454  bnj1014  35457  bnj1408  35532  rankval4b  35594  rdgssun  38119  cpcolld  45069  iunmapss  46032  ssmapsn  46033  sge0iunmpt  47233  sge0iun  47234  voliunsge0lem  47287  omeiunltfirp  47334