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
Assertion
Ref Expression
riotabidva
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem riotabidva
StepHypRef Expression
1 riotabidva.1 . . . . . 6
21pm5.32da 623 . . . . 5
32iotabidv 5439 . . . 4
43ifeq1d 3753 . . 3
51reubidva 2891 . . . 4
65ifbid 3757 . . 3
74, 6eqtrd 2468 . 2
8 df-riota 6549 . 2
9 df-riota 6549 . 2
107, 8, 93eqtr4g 2493 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  cab 2422  wreu 2707  cif 3739  cio 5416  cfv 5454  cund 6541  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