# Metamath Proof Explorer

## Theorem relsnb

Description: An at-most-singleton is a relation iff it is empty (because it is a "singleton on a proper class") or it is a singleton of an ordered pair. (Contributed by BJ, 26-Feb-2023)

Ref Expression
Assertion relsnb ${⊢}\mathrm{Rel}\left\{{A}\right\}↔\left(¬{A}\in \mathrm{V}\vee {A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)$

### Proof

Step Hyp Ref Expression
1 relsng ${⊢}{A}\in \mathrm{V}\to \left(\mathrm{Rel}\left\{{A}\right\}↔{A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)$
2 1 biimpcd ${⊢}\mathrm{Rel}\left\{{A}\right\}\to \left({A}\in \mathrm{V}\to {A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)$
3 imor ${⊢}\left({A}\in \mathrm{V}\to {A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)↔\left(¬{A}\in \mathrm{V}\vee {A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)$
4 2 3 sylib ${⊢}\mathrm{Rel}\left\{{A}\right\}\to \left(¬{A}\in \mathrm{V}\vee {A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)$
5 snprc ${⊢}¬{A}\in \mathrm{V}↔\left\{{A}\right\}=\varnothing$
6 rel0 ${⊢}\mathrm{Rel}\varnothing$
7 releq ${⊢}\left\{{A}\right\}=\varnothing \to \left(\mathrm{Rel}\left\{{A}\right\}↔\mathrm{Rel}\varnothing \right)$
8 6 7 mpbiri ${⊢}\left\{{A}\right\}=\varnothing \to \mathrm{Rel}\left\{{A}\right\}$
9 5 8 sylbi ${⊢}¬{A}\in \mathrm{V}\to \mathrm{Rel}\left\{{A}\right\}$
10 relsng ${⊢}{A}\in \left(\mathrm{V}×\mathrm{V}\right)\to \left(\mathrm{Rel}\left\{{A}\right\}↔{A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)$
11 10 ibir ${⊢}{A}\in \left(\mathrm{V}×\mathrm{V}\right)\to \mathrm{Rel}\left\{{A}\right\}$
12 9 11 jaoi ${⊢}\left(¬{A}\in \mathrm{V}\vee {A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)\to \mathrm{Rel}\left\{{A}\right\}$
13 4 12 impbii ${⊢}\mathrm{Rel}\left\{{A}\right\}↔\left(¬{A}\in \mathrm{V}\vee {A}\in \left(\mathrm{V}×\mathrm{V}\right)\right)$