MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmptf Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 fvmptf.1 . . 3 𝑥𝐴
2 fvmptf.2 . . . . 5 𝑥𝐶
32nfel1 2919 . . . 4 𝑥 𝐶 ∈ V
4 fvmptf.4 . . . . . . 7 𝐹 = (𝑥𝐷𝐵)
5 nfmpt1 5255 . . . . . . 7 𝑥(𝑥𝐷𝐵)
64, 5nfcxfr 2900 . . . . . 6 𝑥𝐹
76, 1nffv 6916 . . . . 5 𝑥(𝐹𝐴)
87, 2nfeq 2916 . . . 4 𝑥(𝐹𝐴) = 𝐶
93, 8nfim 1893 . . 3 𝑥(𝐶 ∈ V → (𝐹𝐴) = 𝐶)
10 fvmptf.3 . . . . 5 (𝑥 = 𝐴𝐵 = 𝐶)
1110eleq1d 2823 . . . 4 (𝑥 = 𝐴 → (𝐵 ∈ V ↔ 𝐶 ∈ V))
12 fveq2 6906 . . . . 5 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
1312, 10eqeq12d 2750 . . . 4 (𝑥 = 𝐴 → ((𝐹𝑥) = 𝐵 ↔ (𝐹𝐴) = 𝐶))
1411, 13imbi12d 344 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ V → (𝐹𝑥) = 𝐵) ↔ (𝐶 ∈ V → (𝐹𝐴) = 𝐶)))
154fvmpt2 7026 . . . 4 ((𝑥𝐷𝐵 ∈ V) → (𝐹𝑥) = 𝐵)
1615ex 412 . . 3 (𝑥𝐷 → (𝐵 ∈ V → (𝐹𝑥) = 𝐵))
171, 9, 14, 16vtoclgaf 3575 . 2 (𝐴𝐷 → (𝐶 ∈ V → (𝐹𝐴) = 𝐶))
18 elex 3498 . 2 (𝐶𝑉𝐶 ∈ V)
1917, 18impel 505 1 ((𝐴𝐷𝐶𝑉) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wnfc 2887  Vcvv 3477  cmpt 5230  cfv 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fv 6570
This theorem is referenced by:  fvmptnf  7037  elfvmptrab1w  7042  elfvmptrab1  7043  elovmpt3rab1  7692  rdgsucmptf  8466  frsucmpt  8476  fprodntriv  15974  prodss  15979  fprodefsum  16127  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem4  26084  dvfsum2  26089  dchrisumlem2  27548  dchrisumlem3  27549  rmfsupp2  33227  ptrest  37605  hlhilset  41916  fsumsermpt  45534  mulc1cncfg  45544  expcnfg  45546  climsubmpt  45615  climeldmeqmpt  45623  climfveqmpt  45626  fnlimfvre  45629  climfveqmpt3  45637  climeldmeqmpt3  45644  climinf2mpt  45669  climinfmpt  45670  stoweidlem23  45978  stoweidlem34  45989  stoweidlem36  45991  wallispilem5  46024  stirlinglem4  46032  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  sge0lempt  46365  sge0isummpt2  46387  meadjiun  46421  hoimbl2  46620  vonhoire  46627
  Copyright terms: Public domain W3C validator