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

Theorem riotabidva 6274
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 3100 analog.) (Contributed by NM, 17-Jan-2012.)
Hypothesis
Ref Expression
riotabidva.1
Assertion
Ref Expression
riotabidva
Distinct variable group:   ,

Proof of Theorem riotabidva
StepHypRef Expression
1 riotabidva.1 . . . 4
21pm5.32da 641 . . 3
32iotabidv 5577 . 2
4 df-riota 6257 . 2
5 df-riota 6257 . 2
63, 4, 53eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  iotacio 5554  iota_crio 6256
This theorem is referenced by:  riotabiia  6275  dfceil2  11968  cidpropd  15105  grpinvpropd  16113  mirval  24036  mirfv  24037  grpoidval  25218  adjval2  26810  xdivval  27615  toslub  27656  tosglb  27658  ringinvval  27782  usgedgvadf1  32415  usgedgvadf1ALT  32418  glbconN  35101  cdlemk33N  36635  cdlemk34  36636  cdlemkid4  36660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250  df-iota 5556  df-riota 6257
  Copyright terms: Public domain W3C validator