brab2d

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	brab2d.1	$⊢ φ \to R = \{⟨x, y⟩ \| ((x \in U \land y \in V) \land ψ)\}$
	brab2d.2	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
Assertion	brab2d	$⊢ φ \to (A R B \leftrightarrow ((A \in U \land B \in V) \land χ))$

Proof

Step	Hyp	Ref	Expression
1		brab2d.1	$⊢ φ \to R = \{⟨x, y⟩ \| ((x \in U \land y \in V) \land ψ)\}$
2		brab2d.2	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
3		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
4	1	eleq2d	$⊢ φ \to (⟨A, B⟩ \in R \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in U \land y \in V) \land ψ)\})$
5	3 4	bitrid	$⊢ φ \to (A R B \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in U \land y \in V) \land ψ)\})$
6		elopab	$⊢ ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in U \land y \in V) \land ψ)\} \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ))$
7	5 6	bitrdi	$⊢ φ \to (A R B \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ)))$
8		eqcom	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \leftrightarrow ⟨A, B⟩ = ⟨x, y⟩$
9		vex	$⊢ x \in V$
10		vex	$⊢ y \in V$
11	9 10	opth	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \leftrightarrow (x = A \land y = B)$
12	8 11	sylbb1	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (x = A \land y = B)$
13		eleq1	$⊢ x = A \to (x \in U \leftrightarrow A \in U)$
14		eleq1	$⊢ y = B \to (y \in V \leftrightarrow B \in V)$
15	13 14	bi2anan9	$⊢ (x = A \land y = B) \to ((x \in U \land y \in V) \leftrightarrow (A \in U \land B \in V))$
16	15	biimpa	$⊢ ((x = A \land y = B) \land (x \in U \land y \in V)) \to (A \in U \land B \in V)$
17	12 16	sylan	$⊢ (⟨A, B⟩ = ⟨x, y⟩ \land (x \in U \land y \in V)) \to (A \in U \land B \in V)$
18	17	adantl	$⊢ (φ \land (⟨A, B⟩ = ⟨x, y⟩ \land (x \in U \land y \in V))) \to (A \in U \land B \in V)$
19	18	adantrrr	$⊢ (φ \land (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ))) \to (A \in U \land B \in V)$
20	19	ex	$⊢ φ \to ((⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ)) \to (A \in U \land B \in V))$
21	20	exlimdvv	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ)) \to (A \in U \land B \in V))$
22	21	imp	$⊢ (φ \land \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ))) \to (A \in U \land B \in V)$
23		simprl	$⊢ (φ \land ((A \in U \land B \in V) \land χ)) \to (A \in U \land B \in V)$
24		simprl	$⊢ (φ \land (A \in U \land B \in V)) \to A \in U$
25		simprr	$⊢ (φ \land (A \in U \land B \in V)) \to B \in V$
26	15	adantl	$⊢ (φ \land (x = A \land y = B)) \to ((x \in U \land y \in V) \leftrightarrow (A \in U \land B \in V))$
27	26 2	anbi12d	$⊢ (φ \land (x = A \land y = B)) \to (((x \in U \land y \in V) \land ψ) \leftrightarrow ((A \in U \land B \in V) \land χ))$
28	27	adantlr	$⊢ ((φ \land (A \in U \land B \in V)) \land (x = A \land y = B)) \to (((x \in U \land y \in V) \land ψ) \leftrightarrow ((A \in U \land B \in V) \land χ))$
29	24 25 28	copsex2dv	$⊢ (φ \land (A \in U \land B \in V)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ)) \leftrightarrow ((A \in U \land B \in V) \land χ))$
30	22 23 29	bibiad	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ((x \in U \land y \in V) \land ψ)) \leftrightarrow ((A \in U \land B \in V) \land χ))$
31	7 30	bitrd	$⊢ φ \to (A R B \leftrightarrow ((A \in U \land B \in V) \land χ))$

Metamath Proof Explorer

Theorem brab2d

Proof