Metamath Proof Explorer
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 ( 𝐵 ↾ 𝐶 ) ) |