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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 ↔ 𝜒 ) )