This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ( 𝐵 ↾ 𝐶 ) ) |