Metamath Proof Explorer

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	$⊢ φ \to R = \{⟨x, y⟩ \| ((x \in C \land y \in D) \land ψ)\}$
		brab2ddw.2	$⊢ x = A \to (ψ \leftrightarrow θ)$
		brab2ddw.3	$⊢ y = B \to (θ \leftrightarrow χ)$
		brab2ddw.4	$⊢ (x = A \land y = B) \to C = U$
		brab2ddw.5	$⊢ (x = A \land y = B) \to D = V$
	Assertion	brab2ddw	$⊢ φ \to (A R B \leftrightarrow ((A \in U \land B \in V) \land χ))$

Proof

Step	Hyp	Ref	Expression
1		brab2dd.1	$⊢ φ \to R = \{⟨x, y⟩ \| ((x \in C \land y \in D) \land ψ)\}$
2		brab2ddw.2	$⊢ x = A \to (ψ \leftrightarrow θ)$
3		brab2ddw.3	$⊢ y = B \to (θ \leftrightarrow χ)$
4		brab2ddw.4	$⊢ (x = A \land y = B) \to C = U$
5		brab2ddw.5	$⊢ (x = A \land y = B) \to D = V$
6	2 3	sylan9bb	$⊢ (x = A \land y = B) \to (ψ \leftrightarrow χ)$
7	6	adantl	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
8		simpl	$⊢ (x = A \land y = B) \to x = A$
9	8 4	eleq12d	$⊢ (x = A \land y = B) \to (x \in C \leftrightarrow A \in U)$
10		simpr	$⊢ (x = A \land y = B) \to y = B$
11	10 5	eleq12d	$⊢ (x = A \land y = B) \to (y \in D \leftrightarrow B \in V)$
12	9 11	anbi12d	$⊢ (x = A \land y = B) \to ((x \in C \land y \in D) \leftrightarrow (A \in U \land B \in V))$
13	12	adantl	$⊢ (φ \land (x = A \land y = B)) \to ((x \in C \land y \in D) \leftrightarrow (A \in U \land B \in V))$
14	1 7 13	brab2dd	$⊢ φ \to (A R B \leftrightarrow ((A \in U \land B \in V) \land χ))$