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 ⊢ ∀ x ∈ A B ∈ V → x ∈ A ⟼ B = x ∈ A ⟼ C ↔ ∀ x ∈ A B = C

Proof

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