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

Proof

Step	Hyp	Ref	Expression
1		nfsymdif.1	⊢ Ⅎ 𝑥 𝐴
2		nfsymdif.2	⊢ Ⅎ 𝑥 𝐵
3		df-symdif	⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
4	1 2	nfdif	⊢ Ⅎ 𝑥 ( 𝐴 ∖ 𝐵 )
5	2 1	nfdif	⊢ Ⅎ 𝑥 ( 𝐵 ∖ 𝐴 )
6	4 5	nfun	⊢ Ⅎ 𝑥 ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
7	3 6	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐴 △ 𝐵 )