Theorem ssiun2 5011

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 3254	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2	1	ex 417	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))
3		eliun 4959	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
4	2, 3	imbitrrdi 255	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
5	4	ssrdv 3942	1 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ∃wrex 3088   ⊆ wss 3904  ∪ ciun 4955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3456  df-ss 3921  df-iun 4957

This theorem is used by:  ssiun2s  5012  disjxiun  5105  triun  5232  iunopeqop  5503  iunopeqopOLD  5504  ixpf  8916  ixpiunwdom  9550  r1sdom  9744  r1val1  9756  rankuni2b  9823  rankval4  9837  cplem1  9877  cplem1OLD  9878  domtriomlem  10432  ac6num  10469  iunfo  10529  iundom2g  10530  pwfseqlem3  10651  inar1  10766  tskuni  10774  iunconnlem  23595  ptclsg  23783  ovoliunlem1  25672  limciun  26064  ssiun2sf  32915  iunxpssiun1  32924  djussxp2  33004  suppovss  33037  bnj906  35327  bnj999  35355  bnj1014  35358  bnj1408  35433  rankval4b  35502  rdgssun  38052  cpcolld  44996  iunmapss  45959  ssmapsn  45960  sge0iunmpt  47160  sge0iun  47161  voliunsge0lem  47214  omeiunltfirp  47261