Theorem ssiun2 5006

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3086   ⊆ wss 3899  ∪ ciun 4951

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 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-ss 3916  df-iun 4953

This theorem is used by:  ssiun2s  5007  disjxiun  5100  triun  5227  iunopeqop  5491  iunopeqopOLD  5492  ixpf  8927  ixpiunwdom  9562  r1sdom  9756  r1val1  9768  rankuni2b  9837  rankval4  9853  cplem1  9907  cplem1OLD  9908  domtriomlem  10477  ac6num  10514  iunfo  10580  iundom2g  10581  pwfseqlem3  10702  inar1  10817  tskuni  10825  iunconnlem  23692  ptclsg  23881  ovoliunlem1  25770  limciun  26161  ssiun2sf  33073  iunxpssiun1  33081  djussxp2  33161  suppovss  33193  bnj906  35480  bnj999  35508  bnj1014  35511  bnj1408  35586  rankval4b  35648  rdgssun  38215  cpcolld  45180  iunmapss  46143  ssmapsn  46144  sge0iunmpt  47344  sge0iun  47345  voliunsge0lem  47398  omeiunltfirp  47445