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

Theorem riotabidva 6068
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 2962 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 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
21pm5.32da 641 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
32iotabidv 5401 . 2  |-  ( ph  ->  ( iota x ( x  e.  A  /\  ps ) )  =  ( iota x ( x  e.  A  /\  ch ) ) )
4 df-riota 6051 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
5 df-riota 6051 . 2  |-  ( iota_ x  e.  A  ch )  =  ( iota x
( x  e.  A  /\  ch ) )
63, 4, 53eqtr4g 2499 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  ( iota_ x  e.  A  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   iotacio 5378   iota_crio 6050
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 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2720  df-uni 4091  df-iota 5380  df-riota 6051
This theorem is referenced by:  riotabiia  6069  dfceil2  11679  cidpropd  14648  grpinvpropd  15600  mirval  23058  mirfv  23059  grpoidval  23702  adjval2  25294  xdivval  26093  toslub  26128  tosglb  26130  rnginvval  26259  glbconN  33019  cdlemk33N  34551  cdlemk34  34552  cdlemkid4  34576
  Copyright terms: Public domain W3C validator