opelopabbv

Description: Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023)

	Ref	Expression
Hypotheses	opelopabbv.def	$⊢ φ \to R = \{⟨x, y⟩ \| ψ\}$
	opelopabbv.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
Assertion	opelopabbv	$⊢ φ \to (⟨A, B⟩ \in R \leftrightarrow ((A \in V \land B \in V) \land χ))$

Step	Hyp	Ref	Expression
1		opelopabbv.def	$⊢ φ \to R = \{⟨x, y⟩ \| ψ\}$
2		opelopabbv.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
3	1	eleq2d	$⊢ φ \to (⟨A, B⟩ \in R \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| ψ\})$
4		ax-5	$⊢ φ \to \forall x φ$
5		ax-5	$⊢ φ \to \forall y φ$
6		nfvd	$⊢ φ \to Ⅎ x χ$
7		nfvd	$⊢ φ \to Ⅎ y χ$
8	4 5 6 7 2	opelopabb	$⊢ φ \to (⟨A, B⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow ((A \in V \land B \in V) \land χ))$
9	3 8	bitrd	$⊢ φ \to (⟨A, B⟩ \in R \leftrightarrow ((A \in V \land B \in V) \land χ))$

Metamath Proof Explorer