ex-opab

Description: Example for df-opab . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)

		Ref	Expression
	Assertion	ex-opab	$⊢ R = \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\} \to 3 R 4$

Step	Hyp	Ref	Expression
1		3cn	$⊢ 3 \in ℂ$
2		4cn	$⊢ 4 \in ℂ$
3		3p1e4	$⊢ 3 + 1 = 4$
4	1	elexi	$⊢ 3 \in V$
5	2	elexi	$⊢ 4 \in V$
6		eleq1	$⊢ x = 3 \to (x \in ℂ \leftrightarrow 3 \in ℂ)$
7		oveq1	$⊢ x = 3 \to x + 1 = 3 + 1$
8	7	eqeq1d	$⊢ x = 3 \to (x + 1 = y \leftrightarrow 3 + 1 = y)$
9	6 8	3anbi13d	$⊢ x = 3 \to ((x \in ℂ \land y \in ℂ \land x + 1 = y) \leftrightarrow (3 \in ℂ \land y \in ℂ \land 3 + 1 = y))$
10		eleq1	$⊢ y = 4 \to (y \in ℂ \leftrightarrow 4 \in ℂ)$
11		eqeq2	$⊢ y = 4 \to (3 + 1 = y \leftrightarrow 3 + 1 = 4)$
12	10 11	3anbi23d	$⊢ y = 4 \to ((3 \in ℂ \land y \in ℂ \land 3 + 1 = y) \leftrightarrow (3 \in ℂ \land 4 \in ℂ \land 3 + 1 = 4))$
13		eqid	$⊢ \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\} = \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\}$
14	4 5 9 12 13	brab	$⊢ 3 \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\} 4 \leftrightarrow (3 \in ℂ \land 4 \in ℂ \land 3 + 1 = 4)$
15	1 2 3 14	mpbir3an	$⊢ 3 \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\} 4$
16		breq	$⊢ R = \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\} \to (3 R 4 \leftrightarrow 3 \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\} 4)$
17	15 16	mpbiri	$⊢ R = \{⟨x, y⟩ \| (x \in ℂ \land y \in ℂ \land x + 1 = y)\} \to 3 R 4$

Metamath Proof Explorer