# Metamath Proof Explorer

## Theorem cnveq0

Description: A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011)

Ref Expression
Assertion cnveq0 ${⊢}\mathrm{Rel}{A}\to \left({A}=\varnothing ↔{{A}}^{-1}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 cnv0 ${⊢}{\varnothing }^{-1}=\varnothing$
2 rel0 ${⊢}\mathrm{Rel}\varnothing$
3 cnveqb ${⊢}\left(\mathrm{Rel}{A}\wedge \mathrm{Rel}\varnothing \right)\to \left({A}=\varnothing ↔{{A}}^{-1}={\varnothing }^{-1}\right)$
4 2 3 mpan2 ${⊢}\mathrm{Rel}{A}\to \left({A}=\varnothing ↔{{A}}^{-1}={\varnothing }^{-1}\right)$
5 eqeq2 ${⊢}\varnothing ={\varnothing }^{-1}\to \left({{A}}^{-1}=\varnothing ↔{{A}}^{-1}={\varnothing }^{-1}\right)$
6 5 bibi2d ${⊢}\varnothing ={\varnothing }^{-1}\to \left(\left({A}=\varnothing ↔{{A}}^{-1}=\varnothing \right)↔\left({A}=\varnothing ↔{{A}}^{-1}={\varnothing }^{-1}\right)\right)$
7 4 6 syl5ibr ${⊢}\varnothing ={\varnothing }^{-1}\to \left(\mathrm{Rel}{A}\to \left({A}=\varnothing ↔{{A}}^{-1}=\varnothing \right)\right)$
8 7 eqcoms ${⊢}{\varnothing }^{-1}=\varnothing \to \left(\mathrm{Rel}{A}\to \left({A}=\varnothing ↔{{A}}^{-1}=\varnothing \right)\right)$
9 1 8 ax-mp ${⊢}\mathrm{Rel}{A}\to \left({A}=\varnothing ↔{{A}}^{-1}=\varnothing \right)$