opelopabb

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

	Ref	Expression
Hypotheses	opelopabb.xph	$⊢ φ \to \forall x φ$
	opelopabb.yph	$⊢ φ \to \forall y φ$
	opelopabb.xch	$⊢ φ \to Ⅎ x χ$
	opelopabb.ych	$⊢ φ \to Ⅎ y χ$
	opelopabb.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
Assertion	opelopabb	$⊢ φ \to (⟨A, B⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow ((A \in V \land B \in V) \land χ))$

Step	Hyp	Ref	Expression
1		opelopabb.xph	$⊢ φ \to \forall x φ$
2		opelopabb.yph	$⊢ φ \to \forall y φ$
3		opelopabb.xch	$⊢ φ \to Ⅎ x χ$
4		opelopabb.ych	$⊢ φ \to Ⅎ y χ$
5		opelopabb.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
6		elopab	$⊢ ⟨A, B⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ)$
7	1 2 3 4 5	copsex2b	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ((A \in V \land B \in V) \land χ))$
8	6 7	bitrid	$⊢ φ \to (⟨A, B⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow ((A \in V \land B \in V) \land χ))$

Metamath Proof Explorer