This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ Ⅎ _ x A
nfsymdif.2 ⊢ Ⅎ _ x B
Assertion nfsymdif ⊢ Ⅎ _ x A ∆ B

Proof

Step Hyp Ref Expression
1 nfsymdif.1 ⊢ Ⅎ _ x A
2 nfsymdif.2 ⊢ Ⅎ _ x B
3 df-symdif ⊢ A ∆ B = A ∖ B ∪ B ∖ A
4 1 2 nfdif ⊢ Ⅎ _ x A ∖ B
5 2 1 nfdif ⊢ Ⅎ _ x B ∖ A
6 4 5 nfun ⊢ Ⅎ _ x A ∖ B ∪ B ∖ A
7 3 6 nfcxfr ⊢ Ⅎ _ x A ∆ B