Theorem fvmptf 6951

Description: Value of a function given by an ordered-pair class abstraction. This version of fvmptg 6928 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)

Hypotheses

Ref	Expression
fvmptf.1	⊢ Ⅎ𝑥𝐴
fvmptf.2	⊢ Ⅎ𝑥𝐶
fvmptf.3	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmptf.4	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)

Assertion

Ref	Expression
fvmptf	⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)

Distinct variable group:   𝑥,𝐷

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptf

Step	Hyp	Ref	Expression
1		fvmptf.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		fvmptf.2	. . . . 5 ⊢ Ⅎ𝑥𝐶
3	2	nfel1 2908	. . . 4 ⊢ Ⅎ𝑥 𝐶 ∈ V
4		fvmptf.4	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
5		nfmpt1 5191	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐷 ↦ 𝐵)
6	4, 5	nfcxfr 2889	. . . . . 6 ⊢ Ⅎ𝑥𝐹
7	6, 1	nffv 6832	. . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝐴)
8	7, 2	nfeq 2905	. . . 4 ⊢ Ⅎ𝑥(𝐹‘𝐴) = 𝐶
9	3, 8	nfim 1896	. . 3 ⊢ Ⅎ𝑥(𝐶 ∈ V → (𝐹‘𝐴) = 𝐶)
10		fvmptf.3	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
11	10	eleq1d 2813	. . . 4 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V ↔ 𝐶 ∈ V))
12		fveq2 6822	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
13	12, 10	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = 𝐵 ↔ (𝐹‘𝐴) = 𝐶))
14	11, 13	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ V → (𝐹‘𝑥) = 𝐵) ↔ (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶)))
15	4	fvmpt2 6941	. . . 4 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝐵 ∈ V) → (𝐹‘𝑥) = 𝐵)
16	15	ex 412	. . 3 ⊢ (𝑥 ∈ 𝐷 → (𝐵 ∈ V → (𝐹‘𝑥) = 𝐵))
17	1, 9, 14, 16	vtoclgaf 3531	. 2 ⊢ (𝐴 ∈ 𝐷 → (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶))
18		elex 3457	. 2 ⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V)
19	17, 18	impel 505	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Ⅎwnfc 2876  Vcvv 3436   ↦ cmpt 5173  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fv 6490

This theorem is referenced by:  fvmptnf  6952  elfvmptrab1w  6957  elfvmptrab1  6958  elovmpt3rab1  7609  rdgsucmptf  8350  frsucmpt  8360  fprodntriv  15849  prodss  15854  fprodefsum  16002  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem4  25934  dvfsum2  25939  dchrisumlem2  27399  dchrisumlem3  27400  rmfsupp2  33179  ptrest  37609  hlhilset  41923  orbitclmpt  44942  fsumsermpt  45570  mulc1cncfg  45580  expcnfg  45582  climsubmpt  45651  climeldmeqmpt  45659  climfveqmpt  45662  fnlimfvre  45665  climfveqmpt3  45673  climeldmeqmpt3  45680  climinf2mpt  45705  climinfmpt  45706  stoweidlem23  46014  stoweidlem34  46025  stoweidlem36  46027  wallispilem5  46060  stirlinglem4  46068  stirlinglem11  46075  stirlinglem12  46076  stirlinglem13  46077  stirlinglem14  46078  sge0lempt  46401  sge0isummpt2  46423  meadjiun  46457  hoimbl2  46656  vonhoire  46663