Theorem brab2ddw

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	brab2dd.1	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) } )
	brab2ddw.2	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
	brab2ddw.3	⊢ ( 𝑦 = 𝐵 → ( 𝜃 ↔ 𝜒 ) )
	brab2ddw.4	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝑈 )
	brab2ddw.5	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐷 = 𝑉 )
Assertion	brab2ddw	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brab2dd.1	⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) } )
2		brab2ddw.2	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
3		brab2ddw.3	⊢ ( 𝑦 = 𝐵 → ( 𝜃 ↔ 𝜒 ) )
4		brab2ddw.4	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝑈 )
5		brab2ddw.5	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐷 = 𝑉 )
6	2 3	sylan9bb	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
8		simpl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 = 𝐴 )
9	8 4	eleq12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝑈 ) )
10		simpr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
11	10 5	eleq12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 ∈ 𝐷 ↔ 𝐵 ∈ 𝑉 ) )
12	9 11	anbi12d	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) )
14	1 7 13	brab2dd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )