Theorem ssiun2 5007

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 416	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4955	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 254	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3944	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2144  ∃wrex 3088   ⊆ wss 3906  ∪ ciun 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rex 3089  df-v 3458  df-ss 3923  df-iun 4953

This theorem is referenced by:  ssiun2s  5008  disjxiun  5099  triun  5224  iunopeqop  5492  iunopeqopOLD  5493  ixpf  8904  ixpiunwdom  9540  r1sdom  9734  r1val1  9746  rankuni2b  9813  rankval4  9827  cplem1  9849  domtriomlem  10401  ac6num  10438  iunfo  10498  iundom2g  10499  pwfseqlem3  10620  inar1  10735  tskuni  10743  iunconnlem  23489  ptclsg  23677  ovoliunlem1  25566  limciun  25958  ssiun2sf  32761  iunxpssiun1  32770  djussxp2  32852  suppovss  32885  bnj906  35227  bnj999  35255  bnj1014  35258  bnj1408  35333  rankval4b  35400  rdgssun  37877  cpcolld  44839  iunmapss  45796  ssmapsn  45797  sge0iunmpt  46997  sge0iun  46998  voliunsge0lem  47051  omeiunltfirp  47098