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 → φ ↔ ψ
bropabg.yB ⊢ y = B → ψ ↔ χ
bropabg.R ⊢ R = x y | φ
Assertion bropabg ⊢ A R B ↔ A ∈ V ∧ B ∈ V ∧ χ

Proof

Step Hyp Ref Expression
1 bropabg.xA ⊢ x = A → φ ↔ ψ
2 bropabg.yB ⊢ y = B → ψ ↔ χ
3 bropabg.R ⊢ R = x y | φ
4 3 bropaex12 ⊢ A R B → A ∈ V ∧ B ∈ V
5 1 2 3 brabg ⊢ A ∈ V ∧ B ∈ V → A R B ↔ χ
6 4 5 biadanii ⊢ A R B ↔ A ∈ V ∧ B ∈ V ∧ χ