Metamath Proof Explorer


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 ( 𝐵𝐶 ) )