This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ◡ ( 𝐴 ∖ 𝐵 ) = ( ◡ 𝐴 ∖ ◡ 𝐵 )