Theorem ssiun3

Description: Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016)

	Ref	Expression
Assertion	ssiun3	⊢ ( ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-ss	⊢ ( 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
2		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐶 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
3		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
4	3	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐶 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
5	1 2 4	3bitr2ri	⊢ ( ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )