Metamath Proof Explorer

Theorem fvmptt

Description: Closed theorem form of fvmpt . (Contributed by Scott Fenton, 21-Feb-2013) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion fvmptt ⊢∀xx=A→B=C∧F=x∈D⟼B∧A∈D∧C∈V→F⁡A=C

Proof

Step Hyp Ref Expression
1 simp2 ⊢∀xx=A→B=C∧F=x∈D⟼B∧A∈D∧C∈V→F=x∈D⟼B
2 1 fveq1d ⊢∀xx=A→B=C∧F=x∈D⟼B∧A∈D∧C∈V→F⁡A=x∈D⟼B⁡A
3 risset ⊢A∈D↔∃x∈Dx=A
4 elex ⊢C∈V→C∈V
5 nfa1 ⊢Ⅎx∀xx=A→B=C
6 nfv ⊢ℲxC∈V
7 nffvmpt1 ⊢Ⅎ_xx∈D⟼B⁡A
8 7 nfeq1 ⊢Ⅎxx∈D⟼B⁡A=C
9 6 8 nfim ⊢ℲxC∈V→x∈D⟼B⁡A=C
10 simprl ⊢x=A∧B=C∧x∈D∧C∈V→x∈D
11 simplr ⊢x=A∧B=C∧x∈D∧C∈V→B=C
12 simprr ⊢x=A∧B=C∧x∈D∧C∈V→C∈V
13 11 12 eqeltrd ⊢x=A∧B=C∧x∈D∧C∈V→B∈V
14 eqid ⊢x∈D⟼B=x∈D⟼B
15 14 fvmpt2 ⊢x∈D∧B∈V→x∈D⟼B⁡x=B
16 10 13 15 syl2anc ⊢x=A∧B=C∧x∈D∧C∈V→x∈D⟼B⁡x=B
17 simpll ⊢x=A∧B=C∧x∈D∧C∈V→x=A
18 17 fveq2d ⊢x=A∧B=C∧x∈D∧C∈V→x∈D⟼B⁡x=x∈D⟼B⁡A
19 16 18 11 3eqtr3d ⊢x=A∧B=C∧x∈D∧C∈V→x∈D⟼B⁡A=C
20 19 exp43 ⊢x=A→B=C→x∈D→C∈V→x∈D⟼B⁡A=C
21 20 a2i ⊢x=A→B=C→x=A→x∈D→C∈V→x∈D⟼B⁡A=C
22 21 com23 ⊢x=A→B=C→x∈D→x=A→C∈V→x∈D⟼B⁡A=C
23 22 sps ⊢∀xx=A→B=C→x∈D→x=A→C∈V→x∈D⟼B⁡A=C
24 5 9 23 rexlimd ⊢∀xx=A→B=C→∃x∈Dx=A→C∈V→x∈D⟼B⁡A=C
25 4 24 syl7 ⊢∀xx=A→B=C→∃x∈Dx=A→C∈V→x∈D⟼B⁡A=C
26 3 25 biimtrid ⊢∀xx=A→B=C→A∈D→C∈V→x∈D⟼B⁡A=C
27 26 imp32 ⊢∀xx=A→B=C∧A∈D∧C∈V→x∈D⟼B⁡A=C
28 27 3adant2 ⊢∀xx=A→B=C∧F=x∈D⟼B∧A∈D∧C∈V→x∈D⟼B⁡A=C
29 2 28 eqtrd ⊢∀xx=A→B=C∧F=x∈D⟼B∧A∈D∧C∈V→F⁡A=C