bj-brab2a1

Description: "Unbounded" version of brab2a . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Hypotheses	bj-brab2a1.1	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
	bj-brab2a1.2	$⊢ R = \{⟨x, y⟩ \| φ\}$
Assertion	bj-brab2a1	$⊢ A R B \leftrightarrow ((A \in V \land B \in V) \land ψ)$

Step	Hyp	Ref	Expression
1		bj-brab2a1.1	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
2		bj-brab2a1.2	$⊢ R = \{⟨x, y⟩ \| φ\}$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	pm3.2i	$⊢ (x \in V \land y \in V)$
6	5	biantrur	$⊢ φ \leftrightarrow ((x \in V \land y \in V) \land φ)$
7	6	opabbii	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨x, y⟩ \| ((x \in V \land y \in V) \land φ)\}$
8	2 7	eqtri	$⊢ R = \{⟨x, y⟩ \| ((x \in V \land y \in V) \land φ)\}$
9	1 8	brab2a	$⊢ A R B \leftrightarrow ((A \in V \land B \in V) \land ψ)$

Metamath Proof Explorer