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

Theorem ovmpt4g 7289
 Description: Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 6772.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypothesis
Ref Expression
ovmpt4g.3 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
Assertion
Ref Expression
ovmpt4g ((𝑥𝐴𝑦𝐵𝐶𝑉) → (𝑥𝐹𝑦) = 𝐶)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem ovmpt4g
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elisset 3504 . . 3 (𝐶𝑉 → ∃𝑧 𝑧 = 𝐶)
2 moeq 3696 . . . . . . 7 ∃*𝑧 𝑧 = 𝐶
32a1i 11 . . . . . 6 ((𝑥𝐴𝑦𝐵) → ∃*𝑧 𝑧 = 𝐶)
4 ovmpt4g.3 . . . . . . 7 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
5 df-mpo 7153 . . . . . . 7 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
64, 5eqtri 2842 . . . . . 6 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
73, 6ovidi 7285 . . . . 5 ((𝑥𝐴𝑦𝐵) → (𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝑧))
8 eqeq2 2831 . . . . 5 (𝑧 = 𝐶 → ((𝑥𝐹𝑦) = 𝑧 ↔ (𝑥𝐹𝑦) = 𝐶))
97, 8mpbidi 243 . . . 4 ((𝑥𝐴𝑦𝐵) → (𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝐶))
109exlimdv 1927 . . 3 ((𝑥𝐴𝑦𝐵) → (∃𝑧 𝑧 = 𝐶 → (𝑥𝐹𝑦) = 𝐶))
111, 10syl5 34 . 2 ((𝑥𝐴𝑦𝐵) → (𝐶𝑉 → (𝑥𝐹𝑦) = 𝐶))
12113impia 1111 1 ((𝑥𝐴𝑦𝐵𝐶𝑉) → (𝑥𝐹𝑦) = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1081   = wceq 1530  ∃wex 1773   ∈ wcel 2107  ∃*wmo 2614  (class class class)co 7148  {coprab 7149   ∈ cmpo 7150 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153 This theorem is referenced by:  ovmpos  7290  ov2gf  7291  ovmpodxf  7292  ovmpodf  7298  ofmres  7677  fnmpoovd  7774  mapxpen  8675  pwfseqlem2  10073  pwfseqlem3  10074  fullfunc  17168  fthfunc  17169  prfcl  17445  curf1cl  17470  curfcl  17474  hofcl  17501  gsum2d2lem  19085  gsum2d2  19086  gsumcom2  19087  dprdval  19117  dprd2d2  19158  cnmpt21  22271  cnmpt2t  22273  cnmptcom  22278  cnmpt2k  22288  xkocnv  22414  suppovss  30418  fedgmullem1  31013  fedgmullem2  31014  fedgmul  31015  madjusmdetlem1  31080  madjusmdetlem3  31082  finxpreclem5  34663  sdclem2  35004  smflimlem1  43032  smflimlem2  43033  aovmpt4g  43385  ovmpordxf  44372
 Copyright terms: Public domain W3C validator