Metamath Proof Explorer

Theorem bropabg

Description: Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt . (Contributed by RP, 26-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		bropabg.xA	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		bropabg.yB	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		bropabg.R	$⊢ R = \{⟨x, y⟩ \| φ\}$
4	3	bropaex12	$⊢ A R B \to (A \in V \land B \in V)$
5	1 2 3	brabg	$⊢ (A \in V \land B \in V) \to (A R B \leftrightarrow χ)$
6	4 5	biadanii	$⊢ A R B \leftrightarrow ((A \in V \land B \in V) \land χ)$