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 ⊢ Ⅎ 𝑥 𝐴
nfres.2 ⊢ Ⅎ 𝑥 𝐵
Assertion nfres Ⅎ 𝑥 ( 𝐴 ↾ 𝐵 )

Proof

Step Hyp Ref Expression
1 nfres.1 ⊢ Ⅎ 𝑥 𝐴
2 nfres.2 ⊢ Ⅎ 𝑥 𝐵
3 df-res ⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
4 nfcv ⊢ Ⅎ 𝑥 V
5 2 4 nfxp ⊢ Ⅎ 𝑥 ( 𝐵 × V )
6 1 5 nfin ⊢ Ⅎ 𝑥 ( 𝐴 ∩ ( 𝐵 × V ) )
7 3 6 nfcxfr ⊢ Ⅎ 𝑥 ( 𝐴 ↾ 𝐵 )