Metamath Proof Explorer

Theorem mpteqb

Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv . (Contributed by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion mpteqb ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
2 1 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
3 fneq1 ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) )
4 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 4 mptfng ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
6 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
7 6 mptfng ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
8 3 5 7 3bitr4g ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ) )
9 8 biimpd ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ) )
10 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ) )
11 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
12 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
13 11 12 nfeq ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
14 simpll ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
15 14 fveq1d ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) )
16 4 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
17 16 ad2ant2lr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
18 6 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ V ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
19 18 ad2ant2l ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
20 15 17 19 3eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐵 = 𝐶 )
21 20 exp31 ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → 𝐵 = 𝐶 ) ) )
22 13 21 ralrimi ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → 𝐵 = 𝐶 ) )
23 ralim ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → 𝐵 = 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )
24 22 23 syl ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )
25 10 24 syl5bir ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ) → ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )
26 25 expd ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V → ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) ) )
27 9 26 mpdd ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )
28 27 com12 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )
29 eqid ⊢ 𝐴 = 𝐴
30 mpteq12 ⊢ ( ( 𝐴 = 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
31 29 30 mpan ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
32 28 31 impbid1 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )
33 2 32 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) )