Theorem nfsymdif

Description: Hypothesis builder for symmetric difference. (Contributed by Scott Fenton, 19-Feb-2013) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	nfsymdif.1	|- F/_ x A
	nfsymdif.2	|- F/_ x B
Assertion	nfsymdif	|- F/_ x ( A /_\ B )

Proof

Step	Hyp	Ref	Expression
1		nfsymdif.1	|- F/_ x A
2		nfsymdif.2	|- F/_ x B
3		df-symdif	|- ( A /_\ B ) = ( ( A \ B ) u. ( B \ A ) )
4	1 2	nfdif	|- F/_ x ( A \ B )
5	2 1	nfdif	|- F/_ x ( B \ A )
6	4 5	nfun	|- F/_ x ( ( A \ B ) u. ( B \ A ) )
7	3 6	nfcxfr	|- F/_ x ( A /_\ B )