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 )