Theorem fvmptf 7036

Description: Value of a function given by an ordered-pair class abstraction. This version of fvmptg 7013 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 2921	. . . 4 ⊢ Ⅎ𝑥 𝐶 ∈ V
4		fvmptf.4	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
5		nfmpt1 5249	. . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐷 ↦ 𝐵)
6	4, 5	nfcxfr 2902	. . . . . 6 ⊢ Ⅎ𝑥𝐹
7	6, 1	nffv 6915	. . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝐴)
8	7, 2	nfeq 2918	. . . 4 ⊢ Ⅎ𝑥(𝐹‘𝐴) = 𝐶
9	3, 8	nfim 1895	. . 3 ⊢ Ⅎ𝑥(𝐶 ∈ V → (𝐹‘𝐴) = 𝐶)
10		fvmptf.3	. . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
11	10	eleq1d 2825	. . . 4 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V ↔ 𝐶 ∈ V))
12		fveq2 6905	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴))
13	12, 10	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = 𝐵 ↔ (𝐹‘𝐴) = 𝐶))
14	11, 13	imbi12d 344	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ V → (𝐹‘𝑥) = 𝐵) ↔ (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶)))
15	4	fvmpt2 7026	. . . 4 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝐵 ∈ V) → (𝐹‘𝑥) = 𝐵)
16	15	ex 412	. . 3 ⊢ (𝑥 ∈ 𝐷 → (𝐵 ∈ V → (𝐹‘𝑥) = 𝐵))
17	1, 9, 14, 16	vtoclgaf 3575	. 2 ⊢ (𝐴 ∈ 𝐷 → (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶))
18		elex 3500	. 2 ⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V)
19	17, 18	impel 505	1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Ⅎwnfc 2889  Vcvv 3479   ↦ cmpt 5224  ‘cfv 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fv 6568

This theorem is referenced by:  fvmptnf  7037  elfvmptrab1w  7042  elfvmptrab1  7043  elovmpt3rab1  7694  rdgsucmptf  8469  frsucmpt  8479  fprodntriv  15979  prodss  15984  fprodefsum  16132  dvfsumabs  26064  dvfsumlem1  26067  dvfsumlem4  26071  dvfsum2  26076  dchrisumlem2  27535  dchrisumlem3  27536  rmfsupp2  33243  ptrest  37627  hlhilset  41937  fsumsermpt  45599  mulc1cncfg  45609  expcnfg  45611  climsubmpt  45680  climeldmeqmpt  45688  climfveqmpt  45691  fnlimfvre  45694  climfveqmpt3  45702  climeldmeqmpt3  45709  climinf2mpt  45734  climinfmpt  45735  stoweidlem23  46043  stoweidlem34  46054  stoweidlem36  46056  wallispilem5  46089  stirlinglem4  46097  stirlinglem11  46104  stirlinglem12  46105  stirlinglem13  46106  stirlinglem14  46107  sge0lempt  46430  sge0isummpt2  46452  meadjiun  46486  hoimbl2  46685  vonhoire  46692