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 ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) } → 3 𝑅 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 ⊢ ( 𝑥 = 3 → ( 𝑥 ∈ ℂ ↔ 3 ∈ ℂ ) )
7 oveq1 ⊢ ( 𝑥 = 3 → ( 𝑥 + 1 ) = ( 3 + 1 ) )
8 7 eqeq1d ⊢ ( 𝑥 = 3 → ( ( 𝑥 + 1 ) = 𝑦 ↔ ( 3 + 1 ) = 𝑦 ) )
9 6 8 3anbi13d ⊢ ( 𝑥 = 3 → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) ↔ ( 3 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 3 + 1 ) = 𝑦 ) ) )
10 eleq1 ⊢ ( 𝑦 = 4 → ( 𝑦 ∈ ℂ ↔ 4 ∈ ℂ ) )
11 eqeq2 ⊢ ( 𝑦 = 4 → ( ( 3 + 1 ) = 𝑦 ↔ ( 3 + 1 ) = 4 ) )
12 10 11 3anbi23d ⊢ ( 𝑦 = 4 → ( ( 3 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 3 + 1 ) = 𝑦 ) ↔ ( 3 ∈ ℂ ∧ 4 ∈ ℂ ∧ ( 3 + 1 ) = 4 ) ) )
13 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) }
14 4 5 9 12 13 brab ⊢ ( 3 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) } 4 ↔ ( 3 ∈ ℂ ∧ 4 ∈ ℂ ∧ ( 3 + 1 ) = 4 ) )
15 1 2 3 14 mpbir3an ⊢ 3 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) } 4
16 breq ⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) } → ( 3 𝑅 4 ↔ 3 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) } 4 ) )
17 15 16 mpbiri ⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝑥 + 1 ) = 𝑦 ) } → 3 𝑅 4 )