Theorem nfdfat

Description: Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g., for Fun/Rel, dom, C_ , etc.). (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	nfdfat.1	⊢ Ⅎ 𝑥 𝐹
	nfdfat.2	⊢ Ⅎ 𝑥 𝐴
Assertion	nfdfat	⊢ Ⅎ 𝑥 𝐹 defAt 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfdfat.1	⊢ Ⅎ 𝑥 𝐹
2		nfdfat.2	⊢ Ⅎ 𝑥 𝐴
3		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
4	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
5	2 4	nfel	⊢ Ⅎ 𝑥 𝐴 ∈ dom 𝐹
6	2	nfsn	⊢ Ⅎ 𝑥 { 𝐴 }
7	1 6	nfres	⊢ Ⅎ 𝑥 ( 𝐹 ↾ { 𝐴 } )
8	7	nffun	⊢ Ⅎ 𝑥 Fun ( 𝐹 ↾ { 𝐴 } )
9	5 8	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) )
10	3 9	nfxfr	⊢ Ⅎ 𝑥 𝐹 defAt 𝐴