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	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	bropabg.yB	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	bropabg.R	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion	bropabg	⊢ ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bropabg.xA	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		bropabg.yB	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3		bropabg.R	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4	3	bropaex12	⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
5	1 2 3	brabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) )
6	4 5	biadanii	⊢ ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜒 ) )