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