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