Metamath Proof Explorer

Theorem brabv

Description: If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017)

		Ref	Expression
	Assertion	brabv	$⊢ X \{⟨x, y⟩ \| φ\} Y \to (X \in V \land Y \in V)$

Proof

Step	Hyp	Ref	Expression
1		df-br	$⊢ X \{⟨x, y⟩ \| φ\} Y \leftrightarrow ⟨X, Y⟩ \in \{⟨x, y⟩ \| φ\}$
2		opprc	$⊢ \neg (X \in V \land Y \in V) \to ⟨X, Y⟩ = \emptyset$
3		0nelopab	$⊢ \neg \emptyset \in \{⟨x, y⟩ \| φ\}$
4		eleq1	$⊢ ⟨X, Y⟩ = \emptyset \to (⟨X, Y⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow \emptyset \in \{⟨x, y⟩ \| φ\})$
5	3 4	mtbiri	$⊢ ⟨X, Y⟩ = \emptyset \to \neg ⟨X, Y⟩ \in \{⟨x, y⟩ \| φ\}$
6	2 5	syl	$⊢ \neg (X \in V \land Y \in V) \to \neg ⟨X, Y⟩ \in \{⟨x, y⟩ \| φ\}$
7	6	con4i	$⊢ ⟨X, Y⟩ \in \{⟨x, y⟩ \| φ\} \to (X \in V \land Y \in V)$
8	1 7	sylbi	$⊢ X \{⟨x, y⟩ \| φ\} Y \to (X \in V \land Y \in V)$