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

Theorem riotabidv 6587
Description: Formula-building deduction rule for restricted iota. (Contributed by NM, 15-Sep-2011.)
Hypothesis
Ref Expression
riotabidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
riotabidv  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  A ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem riotabidv
StepHypRef Expression
1 riotabidv.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21reubidv 2899 . . 3  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
31anbi2d 686 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
43iotabidv 5474 . . 3  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 eqidd 2444 . . 3  |-  ( ph  ->  ( Undef `  { x  |  x  e.  A } )  =  (
Undef `  { x  |  x  e.  A }
) )
62, 4, 5ifbieq12d 3789 . 2  |-  ( ph  ->  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps ) ) ,  (
Undef `  { x  |  x  e.  A }
) )  =  if ( E! x  e.  A  ch ,  ( iota x ( x  e.  A  /\  ch ) ) ,  (
Undef `  { x  |  x  e.  A }
) ) )
7 df-riota 6585 . 2  |-  ( iota_ x  e.  A ps )  =  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps ) ) ,  (
Undef `  { x  |  x  e.  A }
) )
8 df-riota 6585 . 2  |-  ( iota_ x  e.  A ch )  =  if ( E! x  e.  A  ch ,  ( iota x ( x  e.  A  /\  ch ) ) ,  (
Undef `  { x  |  x  e.  A }
) )
96, 7, 83eqtr4g 2500 1  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  A ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1654    e. wcel 1728   {cab 2429   E!wreu 2714   ifcif 3767   iotacio 5451   ` cfv 5489   Undefcund 6577   iota_crio 6578
This theorem is referenced by:  riotaeqbidv  6588  csbriotag  6598  fin23lem27  8246  subval  9335  divval  9718  flval  11241  cjval  11945  sqrval  12080  qnumval  13167  qdenval  13168  lubval  14474  glbval  14479  joinval2  14484  meetval2  14491  spwval2  14694  spwpr4  14701  grpinvval  14882  pj1fval  15364  pj1val  15365  q1pval  20114  coeval  20180  quotval  20247  usgraidx2v  21450  nbgraf1olem4  21492  grpoinvval  21851  pjhval  22937  nmopadjlei  23629  cdj3lem2  23976  cvmliftlem15  25020  cvmlift2lem4  25028  cvmlift2  25038  cvmlift3lem2  25042  cvmlift3lem4  25044  cvmlift3lem6  25046  cvmlift3lem7  25047  cvmlift3lem9  25049  cvmlift3  25050  fvtransport  26001  unxpwdom3  27345  mpaaval  27445  frgra2v  28561  frgrancvvdeqlemB  28599  frgrancvvdeqlemC  28600  lshpkrlem1  30082  lshpkrlem2  30083  lshpkrlem3  30084  lshpkrcl  30088  trlset  31132  trlval  31133  cdleme27b  31339  cdleme29b  31346  cdleme31so  31350  cdleme31sn1  31352  cdleme31sn1c  31359  cdleme31fv  31361  cdlemefrs29clN  31370  cdleme40v  31440  cdlemg1cN  31558  cdlemg1cex  31559  cdlemksv  31815  cdlemkuu  31866  cdlemkid3N  31904  cdlemkid4  31905  cdlemm10N  32090  dicval  32148  dihval  32204  dochfl1  32448  lcfl7N  32473  lcfrlem8  32521  lcfrlem9  32522  lcf1o  32523  mapdhval  32696  hvmapval  32732  hvmapvalvalN  32733  hdmap1fval  32769  hdmap1vallem  32770  hdmap1val  32771  hdmap1cbv  32775  hdmapfval  32802  hdmapval  32803  hgmapffval  32860  hgmapfval  32861  hgmapval  32862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2718  df-reu 2719  df-rab 2721  df-v 2967  df-un 3314  df-if 3768  df-uni 4045  df-iota 5453  df-riota 6585
  Copyright terms: Public domain W3C validator