Theorem ssiun2 4994

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 3222	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 412	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4943	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 252	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3935	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056   ⊆ wss 3897  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-v 3438  df-ss 3914  df-iun 4941

This theorem is referenced by:  ssiun2s  4995  disjxiun  5086  triun  5210  iunopeqop  5459  ixpf  8844  ixpiunwdom  9476  r1sdom  9667  r1val1  9679  rankuni2b  9746  rankval4  9760  cplem1  9782  domtriomlem  10333  ac6num  10370  iunfo  10430  iundom2g  10431  pwfseqlem3  10551  inar1  10666  tskuni  10674  iunconnlem  23342  ptclsg  23530  ovoliunlem1  25430  limciun  25822  ssiun2sf  32539  iunxpssiun1  32548  djussxp2  32630  suppovss  32662  bnj906  34942  bnj999  34970  bnj1014  34973  bnj1408  35048  rankval4b  35111  rdgssun  37422  cpcolld  44350  iunmapss  45311  ssmapsn  45312  sge0iunmpt  46515  sge0iun  46516  voliunsge0lem  46569  omeiunltfirp  46616