# Metamath Proof Explorer

## Theorem 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}=\left\{⟨{x},{y}⟩|\left({x}\in ℂ\wedge {y}\in ℂ\wedge {x}+1={y}\right)\right\}\to 3{R}4$

### Proof

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