Theorem bj-restv

Description: An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uniexr	⊢ ( ∪ 𝑋 ∈ 𝑋 → 𝑋 ∈ V )
2	1	adantl	⊢ ( ( 𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ 𝑋 ) → 𝑋 ∈ V )
3		bj-restb	⊢ ( 𝑋 ∈ V → ( ( 𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ 𝑋 ) → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ) )
4	2 3	mpcom	⊢ ( ( 𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ 𝑋 ) → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) )