Theorem cnvdif

Description: Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014)

	Ref	Expression
Assertion	cnvdif	⊢ ◡ ( 𝐴 ∖ 𝐵 ) = ( ◡ 𝐴 ∖ ◡ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ ( 𝐴 ∖ 𝐵 )
2		difss	⊢ ( ◡ 𝐴 ∖ ◡ 𝐵 ) ⊆ ◡ 𝐴
3		relcnv	⊢ Rel ◡ 𝐴
4		relss	⊢ ( ( ◡ 𝐴 ∖ ◡ 𝐵 ) ⊆ ◡ 𝐴 → ( Rel ◡ 𝐴 → Rel ( ◡ 𝐴 ∖ ◡ 𝐵 ) ) )
5	2 3 4	mp2	⊢ Rel ( ◡ 𝐴 ∖ ◡ 𝐵 )
6		eldif	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	opelcnv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ( 𝐴 ∖ 𝐵 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝐴 ∖ 𝐵 ) )
10		eldif	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐴 ∖ ◡ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐴 ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐵 ) )
11	7 8	opelcnv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐴 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 )
12	7 8	opelcnv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐵 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 )
13	12	notbii	⊢ ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐵 ↔ ¬ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 )
14	11 13	anbi12i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐴 ∧ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝐵 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ) )
15	10 14	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐴 ∖ ◡ 𝐵 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐵 ) )
16	6 9 15	3bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ( 𝐴 ∖ 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐴 ∖ ◡ 𝐵 ) )
17	1 5 16	eqrelriiv	⊢ ◡ ( 𝐴 ∖ 𝐵 ) = ( ◡ 𝐴 ∖ ◡ 𝐵 )