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 2921 . . . 4 𝑥 𝐶 ∈ V
4 fvmptf.4 . . . . . . 7 𝐹 = (𝑥𝐷𝐵)
5 nfmpt1 5249 . . . . . . 7 𝑥(𝑥𝐷𝐵)
64, 5nfcxfr 2902 . . . . . 6 𝑥𝐹
76, 1nffv 6915 . . . . 5 𝑥(𝐹𝐴)
87, 2nfeq 2918 . . . 4 𝑥(𝐹𝐴) = 𝐶
93, 8nfim 1895 . . 3 𝑥(𝐶 ∈ V → (𝐹𝐴) = 𝐶)
10 fvmptf.3 . . . . 5 (𝑥 = 𝐴𝐵 = 𝐶)
1110eleq1d 2825 . . . 4 (𝑥 = 𝐴 → (𝐵 ∈ V ↔ 𝐶 ∈ V))
12 fveq2 6905 . . . . 5 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
1312, 10eqeq12d 2752 . . . 4 (𝑥 = 𝐴 → ((𝐹𝑥) = 𝐵 ↔ (𝐹𝐴) = 𝐶))
1411, 13imbi12d 344 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ V → (𝐹𝑥) = 𝐵) ↔ (𝐶 ∈ V → (𝐹𝐴) = 𝐶)))
154fvmpt2 7026 . . . 4 ((𝑥𝐷𝐵 ∈ V) → (𝐹𝑥) = 𝐵)
1615ex 412 . . 3 (𝑥𝐷 → (𝐵 ∈ V → (𝐹𝑥) = 𝐵))
171, 9, 14, 16vtoclgaf 3575 . 2 (𝐴𝐷 → (𝐶 ∈ V → (𝐹𝐴) = 𝐶))
18 elex 3500 . 2 (𝐶𝑉𝐶 ∈ V)
1917, 18impel 505 1 ((𝐴𝐷𝐶𝑉) → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator