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

Proof

Step Hyp Ref Expression
1 elex ⊢B∈V→B∈V
2 1 ralimi ⊢∀x∈AB∈V→∀x∈AB∈V
3 fneq1 ⊢x∈A⟼B=x∈A⟼C→x∈A⟼BFnA↔x∈A⟼CFnA
4 eqid ⊢x∈A⟼B=x∈A⟼B
5 4 mptfng ⊢∀x∈AB∈V↔x∈A⟼BFnA
6 eqid ⊢x∈A⟼C=x∈A⟼C
7 6 mptfng ⊢∀x∈AC∈V↔x∈A⟼CFnA
8 3 5 7 3bitr4g ⊢x∈A⟼B=x∈A⟼C→∀x∈AB∈V↔∀x∈AC∈V
9 8 biimpd ⊢x∈A⟼B=x∈A⟼C→∀x∈AB∈V→∀x∈AC∈V
10 r19.26 ⊢∀x∈AB∈V∧C∈V↔∀x∈AB∈V∧∀x∈AC∈V
11 nfmpt1 ⊢Ⅎ_xx∈A⟼B
12 nfmpt1 ⊢Ⅎ_xx∈A⟼C
13 11 12 nfeq ⊢Ⅎxx∈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∈AB∈V∧C∈V→B=C
23 ralim ⊢∀x∈AB∈V∧C∈V→B=C→∀x∈AB∈V∧C∈V→∀x∈AB=C
24 22 23 syl ⊢x∈A⟼B=x∈A⟼C→∀x∈AB∈V∧C∈V→∀x∈AB=C
25 10 24 biimtrrid ⊢x∈A⟼B=x∈A⟼C→∀x∈AB∈V∧∀x∈AC∈V→∀x∈AB=C
26 25 expd ⊢x∈A⟼B=x∈A⟼C→∀x∈AB∈V→∀x∈AC∈V→∀x∈AB=C
27 9 26 mpdd ⊢x∈A⟼B=x∈A⟼C→∀x∈AB∈V→∀x∈AB=C
28 27 com12 ⊢∀x∈AB∈V→x∈A⟼B=x∈A⟼C→∀x∈AB=C
29 eqid ⊢A=A
30 mpteq12 ⊢A=A∧∀x∈AB=C→x∈A⟼B=x∈A⟼C
31 29 30 mpan ⊢∀x∈AB=C→x∈A⟼B=x∈A⟼C
32 28 31 impbid1 ⊢∀x∈AB∈V→x∈A⟼B=x∈A⟼C↔∀x∈AB=C
33 2 32 syl ⊢∀x∈AB∈V→x∈A⟼B=x∈A⟼C↔∀x∈AB=C