Theorem nelrnres

Description: If A is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	nelrnres	⊢ ( ¬ 𝐴 ∈ ran 𝐵 → ¬ 𝐴 ∈ ran ( 𝐵 ↾ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rnresss	⊢ ran ( 𝐵 ↾ 𝐶 ) ⊆ ran 𝐵
2		ssnel	⊢ ( ( ran ( 𝐵 ↾ 𝐶 ) ⊆ ran 𝐵 ∧ ¬ 𝐴 ∈ ran 𝐵 ) → ¬ 𝐴 ∈ ran ( 𝐵 ↾ 𝐶 ) )
3	1 2	mpan	⊢ ( ¬ 𝐴 ∈ ran 𝐵 → ¬ 𝐴 ∈ ran ( 𝐵 ↾ 𝐶 ) )