Theorem ssiun2 5005

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086   ⊆ wss 3895  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-ss 3896  df-iun 4952

This theorem is used by:  ssiun2s  5006  disjxiun  5099  triun  5226  iunopeqop  5493  iunopeqopOLD  5494  ixpf  8948  ixpiunwdom  9584  r1sdom  9781  r1val1  9793  rankuni2b  9867  rankval4b  9880  rankval4  9884  cplem1  9950  cplem1OLD  9951  domtriomlem  10520  ac6num  10557  iunfo  10623  iundom2g  10624  pwfseqlem3  10745  inar1  10860  tskuni  10868  iunconnlem  23745  ptclsg  23934  ovoliunlem1  25823  limciun  26214  ssiun2sf  33154  iunxpssiun1  33162  djussxp2  33242  suppovss  33274  bnj906  35560  bnj999  35588  bnj1014  35591  bnj1408  35666  rdgssun  38302  cpcolld  45242  iunmapss  46228  ssmapsn  46229  sge0iunmpt  47428  sge0iun  47429  voliunsge0lem  47482  omeiunltfirp  47529