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

Theorem riotabidv 6551
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 2892 . . 3  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
31anbi2d 685 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
43iotabidv 5439 . . 3  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
5 eqidd 2437 . . 3  |-  ( ph  ->  ( Undef `  { x  |  x  e.  A } )  =  (
Undef `  { x  |  x  e.  A }
) )
62, 4, 5ifbieq12d 3761 . 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 6549 . 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 6549 . 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 2493 1  |-  ( ph  ->  ( iota_ x  e.  A ps )  =  ( iota_ x  e.  A ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   {cab 2422   E!wreu 2707   ifcif 3739   iotacio 5416   ` cfv 5454   Undefcund 6541   iota_crio 6542
This theorem is referenced by:  riotaeqbidv  6552  csbriotag  6562  fin23lem27  8208  subval  9297  divval  9680  flval  11203  cjval  11907  sqrval  12042  qnumval  13129  qdenval  13130  lubval  14436  glbval  14441  joinval2  14446  meetval2  14453  spwval2  14656  spwpr4  14663  grpinvval  14844  pj1fval  15326  pj1val  15327  q1pval  20076  coeval  20142  quotval  20209  usgraidx2v  21412  nbgraf1olem4  21454  grpoinvval  21813  pjhval  22899  nmopadjlei  23591  cdj3lem2  23938  cvmliftlem15  24985  cvmlift2lem4  24993  cvmlift2  25003  cvmlift3lem2  25007  cvmlift3lem4  25009  cvmlift3lem6  25011  cvmlift3lem7  25012  cvmlift3lem9  25014  cvmlift3  25015  fvtransport  25966  unxpwdom3  27233  mpaaval  27333  frgra2v  28389  frgrancvvdeqlemB  28427  frgrancvvdeqlemC  28428  lshpkrlem1  29908  lshpkrlem2  29909  lshpkrlem3  29910  lshpkrcl  29914  trlset  30958  trlval  30959  cdleme27b  31165  cdleme29b  31172  cdleme31so  31176  cdleme31sn1  31178  cdleme31sn1c  31185  cdleme31fv  31187  cdlemefrs29clN  31196  cdleme40v  31266  cdlemg1cN  31384  cdlemg1cex  31385  cdlemksv  31641  cdlemkuu  31692  cdlemkid3N  31730  cdlemkid4  31731  cdlemm10N  31916  dicval  31974  dihval  32030  dochfl1  32274  lcfl7N  32299  lcfrlem8  32347  lcfrlem9  32348  lcf1o  32349  mapdhval  32522  hvmapval  32558  hvmapvalvalN  32559  hdmap1fval  32595  hdmap1vallem  32596  hdmap1val  32597  hdmap1cbv  32601  hdmapfval  32628  hdmapval  32629  hgmapffval  32686  hgmapfval  32687  hgmapval  32688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2958  df-un 3325  df-if 3740  df-uni 4016  df-iota 5418  df-riota 6549
  Copyright terms: Public domain W3C validator