Theorem ssiun2 4991

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062   ⊆ wss 3890  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-ss 3907  df-iun 4936

This theorem is referenced by:  ssiun2s  4992  disjxiun  5083  triun  5208  iunopeqop  5473  ixpf  8865  ixpiunwdom  9502  r1sdom  9695  r1val1  9707  rankuni2b  9774  rankval4  9788  cplem1  9810  domtriomlem  10361  ac6num  10398  iunfo  10458  iundom2g  10459  pwfseqlem3  10580  inar1  10695  tskuni  10703  iunconnlem  23408  ptclsg  23596  ovoliunlem1  25485  limciun  25877  ssiun2sf  32650  iunxpssiun1  32659  djussxp2  32742  suppovss  32775  bnj906  35094  bnj999  35122  bnj1014  35125  bnj1408  35200  rankval4b  35265  rdgssun  37716  cpcolld  44711  iunmapss  45670  ssmapsn  45671  sge0iunmpt  46872  sge0iun  46873  voliunsge0lem  46926  omeiunltfirp  46973