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

Theorem riotabidva 6212
 Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 3049 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 . . . 4
21pm5.32da 639 . . 3
32iotabidv 5510 . 2
4 df-riota 6196 . 2
5 df-riota 6196 . 2
63, 4, 53eqtr4g 2468 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   wceq 1405   wcel 1842  cio 5487  crio 6195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380 This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2759  df-uni 4191  df-iota 5489  df-riota 6196 This theorem is referenced by:  riotabiia  6213  dfceil2  11919  cidpropd  15215  grpinvpropd  16329  mirval  24313  mirfv  24314  grpoidval  25512  adjval2  27103  xdivval  27947  toslub  27988  tosglb  27990  ringinvval  28115  glbconN  32375  cdlemk33N  33909  cdlemk34  33910  cdlemkid4  33934  usgedgvadf1  38024  usgedgvadf1ALT  38027
 Copyright terms: Public domain W3C validator