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

Theorem rdgeq1 6867
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 5690 . . . . . 6  |-  ( F  =  G  ->  ( F `  ( g `  U. dom  g ) )  =  ( G `
 ( g `  U. dom  g ) ) )
21ifeq2d 3808 . . . . 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 3808 . . . 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 4379 . . 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 6833 . . 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 6866 . 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 6866 . 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 2500 1  |-  ( F  =  G  ->  rec ( F ,  A )  =  rec ( G ,  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   _Vcvv 2972   (/)c0 3637   ifcif 3791   U.cuni 4091    e. cmpt 4350   Lim wlim 4720   dom cdm 4840   ran crn 4841   ` cfv 5418  recscrecs 6831   reccrdg 6865
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-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-un 3333  df-if 3792  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-iota 5381  df-fv 5426  df-recs 6832  df-rdg 6866
This theorem is referenced by:  rdgeq12  6869  rdgsucmpt2  6886  frsucmpt2  6895  seqomlem0  6904  omv  6952  oev  6954  dffi3  7681  hsmex  8601  axdc  8690  seqeq2  11810  seqval  11817  trpredlem1  27691  trpredtr  27694  trpredmintr  27695  neibastop2  28582
  Copyright terms: Public domain W3C validator