Metamath Proof Explorer


Theorem fvopab3ig

Description: Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999)

Ref Expression
Hypotheses fvopab3ig.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
fvopab3ig.2 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
fvopab3ig.3 ( 𝑥𝐶 → ∃* 𝑦 𝜑 )
fvopab3ig.4 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) }
Assertion fvopab3ig ( ( 𝐴𝐶𝐵𝐷 ) → ( 𝜒 → ( 𝐹𝐴 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fvopab3ig.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
2 fvopab3ig.2 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
3 fvopab3ig.3 ( 𝑥𝐶 → ∃* 𝑦 𝜑 )
4 fvopab3ig.4 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) }
5 eleq1 ( 𝑥 = 𝐴 → ( 𝑥𝐶𝐴𝐶 ) )
6 5 1 anbi12d ( 𝑥 = 𝐴 → ( ( 𝑥𝐶𝜑 ) ↔ ( 𝐴𝐶𝜓 ) ) )
7 2 anbi2d ( 𝑦 = 𝐵 → ( ( 𝐴𝐶𝜓 ) ↔ ( 𝐴𝐶𝜒 ) ) )
8 6 7 opelopabg ( ( 𝐴𝐶𝐵𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ↔ ( 𝐴𝐶𝜒 ) ) )
9 8 biimpar ( ( ( 𝐴𝐶𝐵𝐷 ) ∧ ( 𝐴𝐶𝜒 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } )
10 9 exp43 ( 𝐴𝐶 → ( 𝐵𝐷 → ( 𝐴𝐶 → ( 𝜒 → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ) ) ) )
11 10 pm2.43a ( 𝐴𝐶 → ( 𝐵𝐷 → ( 𝜒 → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ) ) )
12 11 imp ( ( 𝐴𝐶𝐵𝐷 ) → ( 𝜒 → ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ) )
13 4 fveq1i ( 𝐹𝐴 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ‘ 𝐴 )
14 funopab ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥𝐶𝜑 ) )
15 moanimv ( ∃* 𝑦 ( 𝑥𝐶𝜑 ) ↔ ( 𝑥𝐶 → ∃* 𝑦 𝜑 ) )
16 3 15 mpbir ∃* 𝑦 ( 𝑥𝐶𝜑 )
17 14 16 mpgbir Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) }
18 funopfv ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ‘ 𝐴 ) = 𝐵 ) )
19 17 18 ax-mp ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } ‘ 𝐴 ) = 𝐵 )
20 13 19 eqtrid ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝜑 ) } → ( 𝐹𝐴 ) = 𝐵 )
21 12 20 syl6 ( ( 𝐴𝐶𝐵𝐷 ) → ( 𝜒 → ( 𝐹𝐴 ) = 𝐵 ) )