brabgaf

Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013) (Revised by Thierry Arnoux, 17-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		brabgaf.0	$⊢ Ⅎ x ψ$
2		brabgaf.1	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
3		brabgaf.2	$⊢ R = \{⟨x, y⟩ \| φ\}$
4		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
5	3	eleq2i	$⊢ ⟨A, B⟩ \in R \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| φ\}$
6	4 5	bitri	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| φ\}$
7		elopab	$⊢ ⟨A, B⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ)$
8		elisset	$⊢ A \in V \to \exists x x = A$
9		elisset	$⊢ B \in W \to \exists y y = B$
10		exdistrv	$⊢ \exists x \exists y (x = A \land y = B) \leftrightarrow (\exists x x = A \land \exists y y = B)$
11		nfe1	$⊢ Ⅎ x \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ)$
12	11 1	nfbi	$⊢ Ⅎ x (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
13		nfe1	$⊢ Ⅎ y \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ)$
14	13	nfex	$⊢ Ⅎ y \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ)$
15		nfv	$⊢ Ⅎ y ψ$
16	14 15	nfbi	$⊢ Ⅎ y (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
17		opeq12	$⊢ (x = A \land y = B) \to ⟨x, y⟩ = ⟨A, B⟩$
18		copsexgw	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ))$
19	18	eqcoms	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \to (φ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ))$
20	17 19	syl	$⊢ (x = A \land y = B) \to (φ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ))$
21	20 2	bitr3d	$⊢ (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
22	16 21	exlimi	$⊢ \exists y (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
23	12 22	exlimi	$⊢ \exists x \exists y (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
24	10 23	sylbir	$⊢ (\exists x x = A \land \exists y y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
25	8 9 24	syl2an	$⊢ (A \in V \land B \in W) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
26	7 25	bitrid	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow ψ)$
27	6 26	bitrid	$⊢ (A \in V \land B \in W) \to (A R B \leftrightarrow ψ)$

Metamath Proof Explorer

Theorem brabgaf

Proof