Theorem brabd0

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	brabd0.x	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	brabd0.y	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
	brabd0.xch	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	brabd0.ych	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
	brabd0.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	brabd0.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	brabd0.def	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
	brabd0.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	brabd0	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		brabd0.x	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		brabd0.y	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
3		brabd0.xch	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
4		brabd0.ych	⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
5		brabd0.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
6		brabd0.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7		brabd0.def	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
8		brabd0.is	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
9		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
10	7	eleq2d	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
11	9 10	syl5bb	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
12	1 2 3 4 5 6 8	opelopabd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ 𝜒 ) )
13	11 12	bitrd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) )