Metamath Proof Explorer


Theorem cnvco2

Description: Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Assertion cnvco2 ( 𝐴 𝐵 ) = ( 𝐵 𝐴 )

Proof

Step Hyp Ref Expression
1 relcnv Rel ( 𝐴 𝐵 )
2 relco Rel ( 𝐵 𝐴 )
3 vex 𝑦 ∈ V
4 vex 𝑧 ∈ V
5 3 4 brcnv ( 𝑦 𝐵 𝑧𝑧 𝐵 𝑦 )
6 vex 𝑥 ∈ V
7 6 4 brcnv ( 𝑥 𝐴 𝑧𝑧 𝐴 𝑥 )
8 7 bicomi ( 𝑧 𝐴 𝑥𝑥 𝐴 𝑧 )
9 5 8 anbi12ci ( ( 𝑦 𝐵 𝑧𝑧 𝐴 𝑥 ) ↔ ( 𝑥 𝐴 𝑧𝑧 𝐵 𝑦 ) )
10 9 exbii ( ∃ 𝑧 ( 𝑦 𝐵 𝑧𝑧 𝐴 𝑥 ) ↔ ∃ 𝑧 ( 𝑥 𝐴 𝑧𝑧 𝐵 𝑦 ) )
11 6 3 opelcnv ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 𝐵 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝐴 𝐵 ) )
12 3 6 opelco ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝐴 𝐵 ) ↔ ∃ 𝑧 ( 𝑦 𝐵 𝑧𝑧 𝐴 𝑥 ) )
13 11 12 bitri ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 𝐵 ) ↔ ∃ 𝑧 ( 𝑦 𝐵 𝑧𝑧 𝐴 𝑥 ) )
14 6 3 opelco ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 𝐴 ) ↔ ∃ 𝑧 ( 𝑥 𝐴 𝑧𝑧 𝐵 𝑦 ) )
15 10 13 14 3bitr4i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 𝐴 ) )
16 1 2 15 eqrelriiv ( 𝐴 𝐵 ) = ( 𝐵 𝐴 )