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

Theorem ovmpt4g 6213
Description: Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5781.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypothesis
Ref Expression
ovmpt4g.3  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
Assertion
Ref Expression
ovmpt4g  |-  ( ( x  e.  A  /\  y  e.  B  /\  C  e.  V )  ->  ( x F y )  =  C )
Distinct variable group:    x, y
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)    F( x, y)    V( x, y)

Proof of Theorem ovmpt4g
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 elisset 2983 . . 3  |-  ( C  e.  V  ->  E. z 
z  =  C )
2 moeq 3135 . . . . . . 7  |-  E* z 
z  =  C
32a1i 11 . . . . . 6  |-  ( ( x  e.  A  /\  y  e.  B )  ->  E* z  z  =  C )
4 ovmpt4g.3 . . . . . . 7  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
5 df-mpt2 6096 . . . . . . 7  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
64, 5eqtri 2463 . . . . . 6  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
73, 6ovidi 6209 . . . . 5  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( z  =  C  ->  ( x F y )  =  z ) )
8 eqeq2 2452 . . . . 5  |-  ( z  =  C  ->  (
( x F y )  =  z  <->  ( x F y )  =  C ) )
97, 8mpbidi 216 . . . 4  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( z  =  C  ->  ( x F y )  =  C ) )
109exlimdv 1690 . . 3  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( E. z  z  =  C  ->  (
x F y )  =  C ) )
111, 10syl5 32 . 2  |-  ( ( x  e.  A  /\  y  e.  B )  ->  ( C  e.  V  ->  ( x F y )  =  C ) )
12113impia 1184 1  |-  ( ( x  e.  A  /\  y  e.  B  /\  C  e.  V )  ->  ( x F y )  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369   E.wex 1586    e. wcel 1756   E*wmo 2254  (class class class)co 6091   {coprab 6092    e. cmpt2 6093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-iota 5381  df-fun 5420  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096
This theorem is referenced by:  ovmpt2s  6214  ov2gf  6215  ovmpt2dxf  6216  ovmpt2df  6222  ofmres  6573  fnmpt2ovd  6651  mapxpen  7477  pwfseqlem2  8826  pwfseqlem3  8827  fullfunc  14816  fthfunc  14817  prfcl  15013  curf1cl  15038  curfcl  15042  hofcl  15069  gsum2d2lem  16465  gsum2d2  16466  gsumcom2  16467  dprdval  16485  dprdvalOLD  16487  dprd2d2  16543  cnmpt21  19244  cnmpt2t  19246  cnmptcom  19251  cnmpt2k  19261  xkocnv  19387  sdclem2  28638  aovmpt4g  30107  ovmpt2rdxf  30729
  Copyright terms: Public domain W3C validator