# Metamath Proof Explorer

## Theorem elnonrel

Description: Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020)

Ref Expression
Assertion elnonrel ${⊢}⟨{X},{Y}⟩\in \left({A}\setminus {{{A}}^{-1}}^{-1}\right)↔\left(\varnothing \in {A}\wedge ¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nonrel ${⊢}{A}\setminus {{{A}}^{-1}}^{-1}={A}\setminus \left(\mathrm{V}×\mathrm{V}\right)$
2 1 eleq2i ${⊢}⟨{X},{Y}⟩\in \left({A}\setminus {{{A}}^{-1}}^{-1}\right)↔⟨{X},{Y}⟩\in \left({A}\setminus \left(\mathrm{V}×\mathrm{V}\right)\right)$
3 eldif ${⊢}⟨{X},{Y}⟩\in \left({A}\setminus \left(\mathrm{V}×\mathrm{V}\right)\right)↔\left(⟨{X},{Y}⟩\in {A}\wedge ¬⟨{X},{Y}⟩\in \left(\mathrm{V}×\mathrm{V}\right)\right)$
4 opelxp ${⊢}⟨{X},{Y}⟩\in \left(\mathrm{V}×\mathrm{V}\right)↔\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$
5 4 notbii ${⊢}¬⟨{X},{Y}⟩\in \left(\mathrm{V}×\mathrm{V}\right)↔¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$
6 5 anbi2i ${⊢}\left(⟨{X},{Y}⟩\in {A}\wedge ¬⟨{X},{Y}⟩\in \left(\mathrm{V}×\mathrm{V}\right)\right)↔\left(⟨{X},{Y}⟩\in {A}\wedge ¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\right)$
7 opprc ${⊢}¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\to ⟨{X},{Y}⟩=\varnothing$
8 7 eleq1d ${⊢}¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\to \left(⟨{X},{Y}⟩\in {A}↔\varnothing \in {A}\right)$
9 8 pm5.32ri ${⊢}\left(⟨{X},{Y}⟩\in {A}\wedge ¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\right)↔\left(\varnothing \in {A}\wedge ¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\right)$
10 6 9 bitri ${⊢}\left(⟨{X},{Y}⟩\in {A}\wedge ¬⟨{X},{Y}⟩\in \left(\mathrm{V}×\mathrm{V}\right)\right)↔\left(\varnothing \in {A}\wedge ¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\right)$
11 3 10 bitri ${⊢}⟨{X},{Y}⟩\in \left({A}\setminus \left(\mathrm{V}×\mathrm{V}\right)\right)↔\left(\varnothing \in {A}\wedge ¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\right)$
12 2 11 bitri ${⊢}⟨{X},{Y}⟩\in \left({A}\setminus {{{A}}^{-1}}^{-1}\right)↔\left(\varnothing \in {A}\wedge ¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\right)$