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

Theorem mpteq2ia 3984
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpteq2ia.1  |-  ( x  e.  A  ->  B  =  C )
Assertion
Ref Expression
mpteq2ia  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )

Proof of Theorem mpteq2ia
StepHypRef Expression
1 eqid 2117 . . 3  |-  A  =  A
21ax-gen 1410 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2462 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 3978 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 422 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1314    = wceq 1316    e. wcel 1465   A.wral 2393    |-> cmpt 3959
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-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-ral 2398  df-opab 3960  df-mpt 3961
This theorem is referenced by:  mpteq2i  3985  feqresmpt  5443  elfvmptrab  5484  fmptap  5578  offres  6001  cnrecnv  10650  ege2le3  11304  eirraplem  11410  cnmpt1st  12384  cnmpt2nd  12385  expcncf  12688  dvexp  12771  dveflem  12782  dvef  12783
  Copyright terms: Public domain W3C validator