This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y → 3 R 4

Proof

Step Hyp Ref Expression
1 3cn ⊢ 3 ∈ ℂ
2 4cn ⊢ 4 ∈ ℂ
3 3p1e4 ⊢ 3 + 1 = 4
4 1 elexi ⊢ 3 ∈ V
5 2 elexi ⊢ 4 ∈ V
6 eleq1 ⊢ x = 3 → x ∈ ℂ ↔ 3 ∈ ℂ
7 oveq1 ⊢ x = 3 → x + 1 = 3 + 1
8 7 eqeq1d ⊢ x = 3 → x + 1 = y ↔ 3 + 1 = y
9 6 8 3anbi13d ⊢ x = 3 → x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y ↔ 3 ∈ ℂ ∧ y ∈ ℂ ∧ 3 + 1 = y
10 eleq1 ⊢ y = 4 → y ∈ ℂ ↔ 4 ∈ ℂ
11 eqeq2 ⊢ y = 4 → 3 + 1 = y ↔ 3 + 1 = 4
12 10 11 3anbi23d ⊢ y = 4 → 3 ∈ ℂ ∧ y ∈ ℂ ∧ 3 + 1 = y ↔ 3 ∈ ℂ ∧ 4 ∈ ℂ ∧ 3 + 1 = 4
13 eqid ⊢ x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y = x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y
14 4 5 9 12 13 brab ⊢ 3 x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y 4 ↔ 3 ∈ ℂ ∧ 4 ∈ ℂ ∧ 3 + 1 = 4
15 1 2 3 14 mpbir3an ⊢ 3 x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y 4
16 breq ⊢ R = x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y → 3 R 4 ↔ 3 x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y 4
17 15 16 mpbiri ⊢ R = x y | x ∈ ℂ ∧ y ∈ ℂ ∧ x + 1 = y → 3 R 4