This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brab2ddw2

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	⊢ ( 𝑦 = 𝐵 → ( 𝜃 ↔ 𝜒 ) )
		brab2ddw2.4	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝑈 )
		brab2ddw2.5	⊢ ( 𝑦 = 𝐵 → 𝐷 = 𝑉 )
	Assertion	brab2ddw2	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )

Proof

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