Theorem ssiun2 5014

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054   ⊆ wss 3917  ∪ ciun 4958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3452  df-ss 3934  df-iun 4960

This theorem is referenced by:  ssiun2s  5015  disjxiun  5107  triun  5232  iunopeqop  5484  ixpf  8896  ixpiunwdom  9550  r1sdom  9734  r1val1  9746  rankuni2b  9813  rankval4  9827  cplem1  9849  domtriomlem  10402  ac6num  10439  iunfo  10499  iundom2g  10500  pwfseqlem3  10620  inar1  10735  tskuni  10743  iunconnlem  23321  ptclsg  23509  ovoliunlem1  25410  limciun  25802  ssiun2sf  32495  iunxpssiun1  32504  djussxp2  32579  suppovss  32611  bnj906  34927  bnj999  34955  bnj1014  34958  bnj1408  35033  rdgssun  37373  cpcolld  44254  iunmapss  45216  ssmapsn  45217  sge0iunmpt  46423  sge0iun  46424  voliunsge0lem  46477  omeiunltfirp  46524