Theorem bj-brab2a1

Description: "Unbounded" version of brab2a . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Hypotheses	bj-brab2a1.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
	bj-brab2a1.2	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion	bj-brab2a1	⊢ ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-brab2a1.1	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
2		bj-brab2a1.2	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
3		vex	⊢ 𝑥 ∈ V
4		vex	⊢ 𝑦 ∈ V
5	3 4	pm3.2i	⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
6	5	biantrur	⊢ ( 𝜑 ↔ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ 𝜑 ) )
7	6	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ 𝜑 ) }
8	2 7	eqtri	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ 𝜑 ) }
9	1 8	brab2a	⊢ ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝜓 ) )