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

Theorem riotaeqbidv 6260
 Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
Hypotheses
Ref Expression
riotaeqbidv.1
riotaeqbidv.2
Assertion
Ref Expression
riotaeqbidv
Distinct variable group:   ,

Proof of Theorem riotaeqbidv
StepHypRef Expression
1 riotaeqbidv.2 . . 3
21riotabidv 6259 . 2
3 riotaeqbidv.1 . . 3
43riotaeqdv 6258 . 2
52, 4eqtrd 2498 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  iota_crio 6256 This theorem is referenced by:  dfoi  7957  oieq1  7958  oieq2  7959  ordtypecbv  7963  ordtypelem3  7966  zorn2lem1  8897  zorn2g  8904  cidfval  15073  cidval  15074  cidpropd  15105  lubfval  15608  glbfval  15621  grpinvfval  16088  pj1fval  16712  mpfrcl  18187  evlsval  18188  q1pval  22554  ig1pval  22573  mirval  24036  midf  24142  ismidb  24144  lmif  24151  islmib  24153  gidval  25215  grpoinvfval  25226  pjhfval  26314  cvmliftlem5  28734  cvmliftlem15  28743  trlfset  35885  dicffval  36901  dicfval  36902  dihffval  36957  dihfval  36958  hvmapffval  37485  hvmapfval  37486  hdmap1fval  37524  hdmapffval  37556  hdmapfval  37557  hgmapfval  37616 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