Theorem bj-restuni2

Description: The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni and restuni2 . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restuni2	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋 ) → ∪ ( 𝑋 ↾t 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝑋 ∈ V )
2		ssexg	⊢ ( ( 𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ V ) → 𝐴 ∈ V )
3	1 2	sylan2	⊢ ( ( 𝐴 ⊆ ∪ 𝑋 ∧ 𝑋 ∈ 𝑉 ) → 𝐴 ∈ V )
4	3	ancoms	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋 ) → 𝐴 ∈ V )
5		bj-restuni	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ V ) → ∪ ( 𝑋 ↾t 𝐴 ) = ( ∪ 𝑋 ∩ 𝐴 ) )
6	4 5	syldan	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋 ) → ∪ ( 𝑋 ↾t 𝐴 ) = ( ∪ 𝑋 ∩ 𝐴 ) )
7		inss2	⊢ ( ∪ 𝑋 ∩ 𝐴 ) ⊆ 𝐴
8	7	a1i	⊢ ( 𝐴 ⊆ ∪ 𝑋 → ( ∪ 𝑋 ∩ 𝐴 ) ⊆ 𝐴 )
9		id	⊢ ( 𝐴 ⊆ ∪ 𝑋 → 𝐴 ⊆ ∪ 𝑋 )
10		ssidd	⊢ ( 𝐴 ⊆ ∪ 𝑋 → 𝐴 ⊆ 𝐴 )
11	9 10	ssind	⊢ ( 𝐴 ⊆ ∪ 𝑋 → 𝐴 ⊆ ( ∪ 𝑋 ∩ 𝐴 ) )
12	8 11	eqssd	⊢ ( 𝐴 ⊆ ∪ 𝑋 → ( ∪ 𝑋 ∩ 𝐴 ) = 𝐴 )
13	12	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋 ) → ( ∪ 𝑋 ∩ 𝐴 ) = 𝐴 )
14	6 13	eqtrd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋 ) → ∪ ( 𝑋 ↾t 𝐴 ) = 𝐴 )