Theorem ssiun2 5009

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090   ⊆ wss 3900  ∪ 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4956

This theorem is used by:  ssiun2s  5010  disjxiun  5103  triun  5230  iunopeqop  5498  iunopeqopOLD  5499  ixpf  8973  ixpiunwdom  9608  r1sdom  9805  r1val1  9817  rankuni2b  9891  rankval4b  9904  rankval4  9908  cplem1  9974  cplem1OLD  9975  domtriomlem  10544  ac6num  10581  iunfo  10647  iundom2g  10648  pwfseqlem3  10769  inar1  10884  tskuni  10892  iunconnlem  23772  ptclsg  23961  ovoliunlem1  25850  limciun  26241  ssiun2sf  33223  iunxpssiun1  33231  djussxp2  33311  suppovss  33342  bnj906  35627  bnj999  35655  bnj1014  35658  bnj1408  35733  rdgssun  38492  cpcolld  45432  iunmapss  46431  ssmapsn  46432  sge0iunmpt  47631  sge0iun  47632  voliunsge0lem  47685  omeiunltfirp  47732