brab2dd

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 ψ)\}$
	brab2dd.2	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
	brab2dd.3	$⊢ (φ \land (x = A \land y = B)) \to ((x \in C \land y \in D) \leftrightarrow (A \in U \land B \in V))$
Assertion	brab2dd	$⊢ φ \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		brab2dd.2	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
3		brab2dd.3	$⊢ (φ \land (x = A \land y = B)) \to ((x \in C \land y \in D) \leftrightarrow (A \in U \land B \in V))$
4		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
5	1	eleq2d	$⊢ φ \to (⟨A, B⟩ \in R \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land ψ)\})$
6	4 5	bitrid	$⊢ φ \to (A R B \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land ψ)\})$
7		elopab	$⊢ ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land ψ)\} \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ))$
8	6 7	bitrdi	$⊢ φ \to (A R B \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ)))$
9		simpl	$⊢ (φ \land (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ))) \to φ$
10		eqcom	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \leftrightarrow ⟨A, B⟩ = ⟨x, y⟩$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13	11 12	opth	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \leftrightarrow (x = A \land y = B)$
14	10 13	sylbb1	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (x = A \land y = B)$
15	14	ad2antrl	$⊢ (φ \land (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ))) \to (x = A \land y = B)$
16		simprrl	$⊢ (φ \land (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ))) \to (x \in C \land y \in D)$
17	3	biimpa	$⊢ ((φ \land (x = A \land y = B)) \land (x \in C \land y \in D)) \to (A \in U \land B \in V)$
18	9 15 16 17	syl21anc	$⊢ (φ \land (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ))) \to (A \in U \land B \in V)$
19	18	ex	$⊢ φ \to ((⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ)) \to (A \in U \land B \in V))$
20	19	exlimdvv	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ)) \to (A \in U \land B \in V))$
21	20	imp	$⊢ (φ \land \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ))) \to (A \in U \land B \in V)$
22		simprl	$⊢ (φ \land ((A \in U \land B \in V) \land χ)) \to (A \in U \land B \in V)$
23		simprl	$⊢ (φ \land (A \in U \land B \in V)) \to A \in U$
24		simprr	$⊢ (φ \land (A \in U \land B \in V)) \to B \in V$
25	3 2	anbi12d	$⊢ (φ \land (x = A \land y = B)) \to (((x \in C \land y \in D) \land ψ) \leftrightarrow ((A \in U \land B \in V) \land χ))$
26	25	adantlr	$⊢ ((φ \land (A \in U \land B \in V)) \land (x = A \land y = B)) \to (((x \in C \land y \in D) \land ψ) \leftrightarrow ((A \in U \land B \in V) \land χ))$
27	23 24 26	copsex2dv	$⊢ (φ \land (A \in U \land B \in V)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ)) \leftrightarrow ((A \in U \land B \in V) \land χ))$
28	21 22 27	bibiad	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in C \land y \in D) \land ψ)) \leftrightarrow ((A \in U \land B \in V) \land χ))$
29	8 28	bitrd	$⊢ φ \to (A R B \leftrightarrow ((A \in U \land B \in V) \land χ))$

Metamath Proof Explorer

Theorem brab2dd

Proof