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	$$⊢\underset{\_}{Ⅎ}xA$$
	nfsymdif.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfsymdif	$$⊢\underset{\_}{Ⅎ}x\left(A∆B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfsymdif.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfsymdif.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-symdif	$$⊢\left(A∆B\right)=\left(A\setminus B\right)\cup \left(B\setminus A\right)$$
4	1 2	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(A\setminus B\right)$$
5	2 1	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(B\setminus A\right)$$
6	4 5	nfun	$$⊢\underset{\_}{Ⅎ}x\left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)$$
7	3 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left(A∆B\right)$$