Theorem ssiun2 5049

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 3244	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 411	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 5000	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 251	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3987	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2104  ∃wrex 3068   ⊆ wss 3947  ∪ ciun 4996

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rex 3069  df-v 3474  df-in 3954  df-ss 3964  df-iun 4998

This theorem is referenced by:  ssiun2s  5050  disjxiun  5144  triun  5279  iunopeqop  5520  ixpf  8916  ixpiunwdom  9587  r1sdom  9771  r1val1  9783  rankuni2b  9850  rankval4  9864  cplem1  9886  domtriomlem  10439  ac6num  10476  iunfo  10536  iundom2g  10537  pwfseqlem3  10657  inar1  10772  tskuni  10780  iunconnlem  23151  ptclsg  23339  ovoliunlem1  25251  limciun  25643  ssiun2sf  32058  djussxp2  32140  suppovss  32173  bnj906  34239  bnj999  34267  bnj1014  34270  bnj1408  34345  rdgssun  36562  cpcolld  43319  iunmapss  44212  ssmapsn  44213  sge0iunmpt  45432  sge0iun  45433  voliunsge0lem  45486  omeiunltfirp  45533