ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fvmptg Unicode version

Theorem fvmptg 5501
Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptg.1  |-  ( x  =  A  ->  B  =  C )
fvmptg.2  |-  F  =  ( x  e.  D  |->  B )
Assertion
Ref Expression
fvmptg  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( F `  A
)  =  C )
Distinct variable groups:    x, A    x, C    x, D
Allowed substitution hints:    B( x)    R( x)    F( x)

Proof of Theorem fvmptg
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eqid 2140 . 2  |-  C  =  C
2 fvmptg.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
32eqeq2d 2152 . . 3  |-  ( x  =  A  ->  (
y  =  B  <->  y  =  C ) )
4 eqeq1 2147 . . 3  |-  ( y  =  C  ->  (
y  =  C  <->  C  =  C ) )
5 moeq 2860 . . . 4  |-  E* y 
y  =  B
65a1i 9 . . 3  |-  ( x  e.  D  ->  E* y  y  =  B
)
7 fvmptg.2 . . . 4  |-  F  =  ( x  e.  D  |->  B )
8 df-mpt 3995 . . . 4  |-  ( x  e.  D  |->  B )  =  { <. x ,  y >.  |  ( x  e.  D  /\  y  =  B ) }
97, 8eqtri 2161 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  D  /\  y  =  B ) }
103, 4, 6, 9fvopab3ig 5499 . 2  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( C  =  C  ->  ( F `  A )  =  C ) )
111, 10mpi 15 1  |-  ( ( A  e.  D  /\  C  e.  R )  ->  ( F `  A
)  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1332    e. wcel 1481   E*wmo 2001   {copab 3992    |-> cmpt 3993   ` cfv 5127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4050  ax-pow 4102  ax-pr 4135
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2689  df-sbc 2911  df-un 3076  df-in 3078  df-ss 3085  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-br 3934  df-opab 3994  df-mpt 3995  df-id 4219  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-iota 5092  df-fun 5129  df-fv 5135
This theorem is referenced by:  fvmpt  5502  fvmpts  5503  fvmpt3  5504  fvmpt2  5508  f1mpt  5676  caofinvl  6008  1stvalg  6044  2ndvalg  6045  brtpos2  6152  rdgon  6287  frec0g  6298  freccllem  6303  frecfcllem  6305  frecsuclem  6307  sucinc  6345  sucinc2  6346  omcl  6361  oeicl  6362  oav2  6363  omv2  6365  fvdiagfn  6591  djulclr  6938  djurclr  6939  djulcl  6940  djurcl  6941  djulclb  6944  omp1eomlem  6983  ctmlemr  6997  nnnninf  7027  cardval3ex  7054  ceilqval  10106  frec2uzzd  10200  frec2uzsucd  10201  monoord2  10277  iseqf1olemqval  10287  iseqf1olemqk  10294  seq3f1olemqsum  10300  seq3f1oleml  10303  seq3f1o  10304  seq3distr  10313  ser3le  10318  hashinfom  10552  hashennn  10554  cjval  10645  reval  10649  imval  10650  cvg1nlemcau  10784  cvg1nlemres  10785  absval  10801  resqrexlemglsq  10822  resqrexlemga  10823  climmpt  11097  climle  11131  climcvg1nlem  11146  summodclem3  11177  summodclem2a  11178  zsumdc  11181  fsum3  11184  fsumcl2lem  11195  sumsnf  11206  isumadd  11228  fsumrev  11240  fsumshft  11241  fsummulc2  11245  iserabs  11272  isumlessdc  11293  divcnv  11294  trireciplem  11297  trirecip  11298  expcnvap0  11299  expcnvre  11300  expcnv  11301  explecnv  11302  geolim  11308  geolim2  11309  geo2lim  11313  geoisum  11314  geoisumr  11315  geoisum1  11316  geoisum1c  11317  cvgratz  11329  mertenslem2  11333  mertensabs  11334  eftvalcn  11391  efval  11395  efcvgfsum  11401  ege2le3  11405  efcj  11407  eftlub  11424  efgt1p2  11429  eflegeo  11435  sinval  11436  cosval  11437  tanvalap  11442  eirraplem  11510  phival  11916  crth  11927  phimullem  11928  ennnfonelemj0  11941  ennnfonelem0  11945  strnfvnd  12009  topnvalg  12162  toponsspwpwg  12219  tgval  12248  cldval  12298  ntrfval  12299  clsfval  12300  neifval  12339  neival  12342  ismet  12543  isxmet  12544  divcnap  12754  mulc1cncf  12775  djucllem  13161  nnsf  13357  peano3nninf  13359  nninfalllemn  13360  nninfself  13367  nninfsellemeqinf  13370  dcapncf  13406
  Copyright terms: Public domain W3C validator