Theorem fvopab3g

Description: Value of a function given by ordered-pair class abstraction. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Hypotheses	fvopab3g.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	fvopab3g.3	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	fvopab3g.4	⊢ ( 𝑥 ∈ 𝐶 → ∃! 𝑦 𝜑 )
	fvopab3g.5	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) }
Assertion	fvopab3g	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		fvopab3g.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		fvopab3g.3	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3		fvopab3g.4	⊢ ( 𝑥 ∈ 𝐶 → ∃! 𝑦 𝜑 )
4		fvopab3g.5	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) }
5		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) )
6	5 1	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜓 ) ) )
7	2	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝐶 ∧ 𝜓 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜒 ) ) )
8	6 7	opelopabg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜒 ) ) )
9	3 4	fnopab	⊢ 𝐹 Fn 𝐶
10		fnopfvb	⊢ ( ( 𝐹 Fn 𝐶 ∧ 𝐴 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ) )
11	9 10	mpan	⊢ ( 𝐴 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ) )
12	4	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } )
13	11 12	bitrdi	⊢ ( 𝐴 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ) )
14	13	adantr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜑 ) } ) )
15		ibar	⊢ ( 𝐴 ∈ 𝐶 → ( 𝜒 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜒 ) ) )
16	15	adantr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝜒 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝜒 ) ) )
17	8 14 16	3bitr4d	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ 𝜒 ) )