This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfres

Description: Bound-variable hypothesis builder for restriction. (Contributed by NM, 15-Sep-2003) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypotheses nfres.1 ⊢ Ⅎ _ x A
nfres.2 ⊢ Ⅎ _ x B
Assertion nfres ⊢ Ⅎ _ x A ↾ B

Proof

Step Hyp Ref Expression
1 nfres.1 ⊢ Ⅎ _ x A
2 nfres.2 ⊢ Ⅎ _ x B
3 df-res ⊢ A ↾ B = A ∩ B × V
4 nfcv ⊢ Ⅎ _ x V
5 2 4 nfxp ⊢ Ⅎ _ x B × V
6 1 5 nfin ⊢ Ⅎ _ x A ∩ B × V
7 3 6 nfcxfr ⊢ Ⅎ _ x A ↾ B