Theorem bj-resta

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

	Ref	Expression
Assertion	bj-resta	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐴 ∈ 𝑋 → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ 𝐴 ⊆ 𝐴
2		bj-restb	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ) )
3	1 2	mpani	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐴 ∈ 𝑋 → 𝐴 ∈ ( 𝑋 ↾t 𝐴 ) ) )