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 (A ∖ {A^{-1}}^{-1}) \leftrightarrow (\emptyset \in A \land \neg (X \in V \land Y \in V))$

Proof

Step	Hyp	Ref	Expression
1		nonrel	$⊢ A ∖ {A^{-1}}^{-1} = A ∖ (V \times V)$
2	1	eleq2i	$⊢ ⟨X, Y⟩ \in (A ∖ {A^{-1}}^{-1}) \leftrightarrow ⟨X, Y⟩ \in (A ∖ (V \times V))$
3		eldif	$⊢ ⟨X, Y⟩ \in (A ∖ (V \times V)) \leftrightarrow (⟨X, Y⟩ \in A \land \neg ⟨X, Y⟩ \in (V \times V))$
4		opelxp	$⊢ ⟨X, Y⟩ \in (V \times V) \leftrightarrow (X \in V \land Y \in V)$
5	4	notbii	$⊢ \neg ⟨X, Y⟩ \in (V \times V) \leftrightarrow \neg (X \in V \land Y \in V)$
6	5	anbi2i	$⊢ (⟨X, Y⟩ \in A \land \neg ⟨X, Y⟩ \in (V \times V)) \leftrightarrow (⟨X, Y⟩ \in A \land \neg (X \in V \land Y \in V))$
7		opprc	$⊢ \neg (X \in V \land Y \in V) \to ⟨X, Y⟩ = \emptyset$
8	7	eleq1d	$⊢ \neg (X \in V \land Y \in V) \to (⟨X, Y⟩ \in A \leftrightarrow \emptyset \in A)$
9	8	pm5.32ri	$⊢ (⟨X, Y⟩ \in A \land \neg (X \in V \land Y \in V)) \leftrightarrow (\emptyset \in A \land \neg (X \in V \land Y \in V))$
10	6 9	bitri	$⊢ (⟨X, Y⟩ \in A \land \neg ⟨X, Y⟩ \in (V \times V)) \leftrightarrow (\emptyset \in A \land \neg (X \in V \land Y \in V))$
11	3 10	bitri	$⊢ ⟨X, Y⟩ \in (A ∖ (V \times V)) \leftrightarrow (\emptyset \in A \land \neg (X \in V \land Y \in V))$
12	2 11	bitri	$⊢ ⟨X, Y⟩ \in (A ∖ {A^{-1}}^{-1}) \leftrightarrow (\emptyset \in A \land \neg (X \in V \land Y \in V))$