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	|- F/_ x F
	nfdfat.2	|- F/_ x A
Assertion	nfdfat	|- F/ x F defAt A

Proof

Step	Hyp	Ref	Expression
1		nfdfat.1	|- F/_ x F
2		nfdfat.2	|- F/_ x A
3		df-dfat	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
4	1	nfdm	|- F/_ x dom F
5	2 4	nfel	|- F/ x A e. dom F
6	2	nfsn	|- F/_ x { A }
7	1 6	nfres	|- F/_ x ( F |` { A } )
8	7	nffun	|- F/ x Fun ( F |` { A } )
9	5 8	nfan	|- F/ x ( A e. dom F /\ Fun ( F |` { A } ) )
10	3 9	nfxfr	|- F/ x F defAt A