Theorem ssiun2 4990

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061   ⊆ wss 3889  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  ssiun2s  4991  disjxiun  5082  triun  5207  iunopeqop  5475  iunopeqopOLD  5476  ixpf  8868  ixpiunwdom  9505  r1sdom  9698  r1val1  9710  rankuni2b  9777  rankval4  9791  cplem1  9813  domtriomlem  10364  ac6num  10401  iunfo  10461  iundom2g  10462  pwfseqlem3  10583  inar1  10698  tskuni  10706  iunconnlem  23392  ptclsg  23580  ovoliunlem1  25469  limciun  25861  ssiun2sf  32629  iunxpssiun1  32638  djussxp2  32721  suppovss  32754  bnj906  35072  bnj999  35100  bnj1014  35103  bnj1408  35178  rankval4b  35243  rdgssun  37694  cpcolld  44685  iunmapss  45644  ssmapsn  45645  sge0iunmpt  46846  sge0iun  46847  voliunsge0lem  46900  omeiunltfirp  46947