Theorem fvopab6

Description: Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvopab6.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐵 ) }
	fvopab6.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	fvopab6.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion	fvopab6	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvopab6.1	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐵 ) }
2		fvopab6.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		fvopab6.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4		elex	⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ∈ V )
5	3	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝑦 = 𝐶 ) )
6	2 5	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ 𝑦 = 𝐵 ) ↔ ( 𝜓 ∧ 𝑦 = 𝐶 ) ) )
7		iba	⊢ ( 𝑦 = 𝐶 → ( 𝜓 ↔ ( 𝜓 ∧ 𝑦 = 𝐶 ) ) )
8	7	bicomd	⊢ ( 𝑦 = 𝐶 → ( ( 𝜓 ∧ 𝑦 = 𝐶 ) ↔ 𝜓 ) )
9		moeq	⊢ ∃* 𝑦 𝑦 = 𝐵
10	9	moani	⊢ ∃* 𝑦 ( 𝜑 ∧ 𝑦 = 𝐵 )
11	10	a1i	⊢ ( 𝑥 ∈ V → ∃* 𝑦 ( 𝜑 ∧ 𝑦 = 𝐵 ) )
12		vex	⊢ 𝑥 ∈ V
13	12	biantrur	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ V ∧ ( 𝜑 ∧ 𝑦 = 𝐵 ) ) )
14	13	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ ( 𝜑 ∧ 𝑦 = 𝐵 ) ) }
15	1 14	eqtri	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ ( 𝜑 ∧ 𝑦 = 𝐵 ) ) }
16	6 8 11 15	fvopab3ig	⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑅 ) → ( 𝜓 → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) )
17	4 16	sylan	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ) → ( 𝜓 → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) )
18	17	3impia	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )