Theorem ssiun2 4996

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053   ⊆ wss 3903  ∪ ciun 4941

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3438  df-ss 3920  df-iun 4943

This theorem is referenced by:  ssiun2s  4997  disjxiun  5089  triun  5213  iunopeqop  5464  ixpf  8847  ixpiunwdom  9482  r1sdom  9670  r1val1  9682  rankuni2b  9749  rankval4  9763  cplem1  9785  domtriomlem  10336  ac6num  10373  iunfo  10433  iundom2g  10434  pwfseqlem3  10554  inar1  10669  tskuni  10677  iunconnlem  23312  ptclsg  23500  ovoliunlem1  25401  limciun  25793  ssiun2sf  32508  iunxpssiun1  32517  djussxp2  32599  suppovss  32631  bnj906  34913  bnj999  34941  bnj1014  34944  bnj1408  35019  rdgssun  37372  cpcolld  44251  iunmapss  45213  ssmapsn  45214  sge0iunmpt  46419  sge0iun  46420  voliunsge0lem  46473  omeiunltfirp  46520