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

Theorem rdgeq1 6995
Description: Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
Assertion
Ref Expression
rdgeq1  |-  ( F  =  G  ->  rec ( F ,  A )  =  rec ( G ,  A ) )

Proof of Theorem rdgeq1
Dummy variable  g is distinct from all other variables.
StepHypRef Expression
1 fveq1 5773 . . . . . 6  |-  ( F  =  G  ->  ( F `  ( g `  U. dom  g ) )  =  ( G `
 ( g `  U. dom  g ) ) )
21ifeq2d 3876 . . . . 5  |-  ( F  =  G  ->  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) )  =  if ( Lim  dom  g ,  U. ran  g ,  ( G `  ( g `  U. dom  g ) ) ) )
32ifeq2d 3876 . . . 4  |-  ( F  =  G  ->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) )  =  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( G `  (
g `  U. dom  g
) ) ) ) )
43mpteq2dv 4454 . . 3  |-  ( F  =  G  ->  (
g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) )  =  ( g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( G `  ( g `  U. dom  g ) ) ) ) ) )
5 recseq 6961 . . 3  |-  ( ( g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) )  =  ( g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( G `  ( g `  U. dom  g ) ) ) ) )  -> recs ( ( g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) ) )  = recs (
( g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( G `  ( g `
 U. dom  g
) ) ) ) ) ) )
64, 5syl 16 . 2  |-  ( F  =  G  -> recs ( ( g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  ( g `
 U. dom  g
) ) ) ) ) )  = recs (
( g  e.  _V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( G `  ( g `
 U. dom  g
) ) ) ) ) ) )
7 df-rdg 6994 . 2  |-  rec ( F ,  A )  = recs ( ( g  e. 
_V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( F `  (
g `  U. dom  g
) ) ) ) ) )
8 df-rdg 6994 . 2  |-  rec ( G ,  A )  = recs ( ( g  e. 
_V  |->  if ( g  =  (/) ,  A ,  if ( Lim  dom  g ,  U. ran  g ,  ( G `  (
g `  U. dom  g
) ) ) ) ) )
96, 7, 83eqtr4g 2448 1  |-  ( F  =  G  ->  rec ( F ,  A )  =  rec ( G ,  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   _Vcvv 3034   (/)c0 3711   ifcif 3857   U.cuni 4163    |-> cmpt 4425   Lim wlim 4793   dom cdm 4913   ran crn 4914   ` cfv 5496  recscrecs 6959   reccrdg 6993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-un 3394  df-if 3858  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-iota 5460  df-fv 5504  df-recs 6960  df-rdg 6994
This theorem is referenced by:  rdgeq12  6997  rdgsucmpt2  7014  frsucmpt2  7023  seqomlem0  7032  omv  7080  oev  7082  dffi3  7806  hsmex  8725  axdc  8814  seqeq2  12014  seqval  12021  trpredlem1  29475  trpredtr  29478  trpredmintr  29479  neibastop2  30345
  Copyright terms: Public domain W3C validator