This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssiun2sf

Description: Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016)

Ref Expression
Hypotheses ssiun2sf.1 ⊢ Ⅎ 𝑥 𝐴
ssiun2sf.2 ⊢ Ⅎ 𝑥 𝐶
ssiun2sf.3 ⊢ Ⅎ 𝑥 𝐷
ssiun2sf.4 ⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
Assertion ssiun2sf ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 ssiun2sf.1 ⊢ Ⅎ 𝑥 𝐴
2 ssiun2sf.2 ⊢ Ⅎ 𝑥 𝐶
3 ssiun2sf.3 ⊢ Ⅎ 𝑥 𝐷
4 ssiun2sf.4 ⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
5 2 1 nfel ⊢ Ⅎ 𝑥 𝐶 ∈ 𝐴
6 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
7 3 6 nfss ⊢ Ⅎ 𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
8 5 7 nfim ⊢ Ⅎ 𝑥 ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
9 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
10 4 sseq1d ⊢ ( 𝑥 = 𝐶 → ( 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
11 9 10 imbi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) )
12 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
13 2 8 11 12 vtoclgf ⊢ ( 𝐶 ∈ 𝐴 → ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
14 13 pm2.43i ⊢ ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )