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

Theorem riotabidva 6566
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 2947 analog.) (Contributed by NM, 17-Jan-2012.)
Hypothesis
Ref Expression
riotabidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
riotabidva  |-  ( 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 riotabidva
StepHypRef Expression
1 riotabidva.1 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
21pm5.32da 623 . . . . 5  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
32iotabidv 5439 . . . 4  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
43ifeq1d 3753 . . 3  |-  ( ph  ->  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps ) ) ,  (
Undef `  { x  |  x  e.  A }
) )  =  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ch ) ) ,  (
Undef `  { x  |  x  e.  A }
) ) )
51reubidva 2891 . . . 4  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
65ifbid 3757 . . 3  |-  ( ph  ->  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ch ) ) ,  (
Undef `  { x  |  x  e.  A }
) )  =  if ( E! x  e.  A  ch ,  ( iota x ( x  e.  A  /\  ch ) ) ,  (
Undef `  { x  |  x  e.  A }
) ) )
74, 6eqtrd 2468 . 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 }
) ) )
8 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 }
) )
9 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 }
) )
107, 8, 93eqtr4g 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:  riotabiia  6567  cidpropd  13936  grpinvpropd  14866  grpoidval  21804  adjval2  23394  xdivval  24165  toslub  24191  tosglb  24192  rnginvval  24228  glbconN  30174  cdlemk33N  31706  cdlemk34  31707  cdlemkid4  31731
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