Theorem brsymdif

Description: Characterization of the symmetric difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	brsymdif	⊢ ( 𝐴 ( 𝑅 △ 𝑆 ) 𝐵 ↔ ¬ ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑆 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐴 ( 𝑅 △ 𝑆 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 △ 𝑆 ) )
2		elsymdif	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 △ 𝑆 ) ↔ ¬ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑆 ) )
3		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
4		df-br	⊢ ( 𝐴 𝑆 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑆 )
5	3 4	bibi12i	⊢ ( ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑆 𝐵 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑆 ) )
6	2 5	xchbinxr	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 △ 𝑆 ) ↔ ¬ ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑆 𝐵 ) )
7	1 6	bitri	⊢ ( 𝐴 ( 𝑅 △ 𝑆 ) 𝐵 ↔ ¬ ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑆 𝐵 ) )