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