Theorem ssiun2 4981

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 3234	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 412	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4933	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	syl6ibr 251	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3931	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3066   ⊆ wss 3891  ∪ ciun 4929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3432  df-in 3898  df-ss 3908  df-iun 4931

This theorem is referenced by:  ssiun2s  4982  disjxiun  5075  triun  5208  iunopeqop  5437  ixpf  8682  ixpiunwdom  9310  trpredrec  9467  r1sdom  9516  r1val1  9528  rankuni2b  9595  rankval4  9609  cplem1  9631  domtriomlem  10182  ac6num  10219  iunfo  10279  iundom2g  10280  pwfseqlem3  10400  inar1  10515  tskuni  10523  iunconnlem  22559  ptclsg  22747  ovoliunlem1  24647  limciun  25039  ssiun2sf  30878  djussxp2  30964  suppovss  30996  bnj906  32889  bnj999  32917  bnj1014  32920  bnj1408  32995  rdgssun  35528  cpcolld  41829  iunmapss  42708  ssmapsn  42709  sge0iunmpt  43910  sge0iun  43911  voliunsge0lem  43964  omeiunltfirp  44011