Theorem brabd

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023)

	Ref	Expression
Hypotheses	brabd.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	brabd.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	brabd.def	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
	brabd.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	brabd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		brabd.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		brabd.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		brabd.def	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
4		brabd.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
5		ax-5	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
6		ax-5	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
7		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
8		nfvd	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
9	5 6 7 8 1 2 3 4	brabd0	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) )