Theorem ssiun2 5017

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

Syntax hints:   → wi 4   ∈ wcel 2150  ∃wrex 3096   ⊆ wss 3913  ∪ ciun 4961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-12 2220  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-rex 3097  df-v 3464  df-ss 3930  df-iun 4963

This theorem is referenced by:  ssiun2s  5018  disjxiun  5111  triun  5238  iunopeqop  5508  iunopeqopOLD  5509  ixpf  8921  ixpiunwdom  9555  r1sdom  9749  r1val1  9761  rankuni2b  9828  rankval4  9842  cplem1  9878  domtriomlem  10429  ac6num  10466  iunfo  10526  iundom2g  10527  pwfseqlem3  10648  inar1  10763  tskuni  10771  iunconnlem  23567  ptclsg  23755  ovoliunlem1  25644  limciun  26036  ssiun2sf  32874  iunxpssiun1  32883  djussxp2  32963  suppovss  32996  bnj906  35288  bnj999  35316  bnj1014  35319  bnj1408  35394  rankval4b  35461  rdgssun  37972  cpcolld  44920  iunmapss  45883  ssmapsn  45884  sge0iunmpt  47084  sge0iun  47085  voliunsge0lem  47138  omeiunltfirp  47185