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

Theorem riota2 6280
Description: This theorem shows a condition that allows us to represent a descriptor with a class expression . (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
Hypothesis
Ref Expression
riota2.1
Assertion
Ref Expression
riota2
Distinct variable groups:   ,   ,   ,

Proof of Theorem riota2
StepHypRef Expression
1 nfcv 2619 . 2
2 nfv 1707 . 2
3 riota2.1 . 2
41, 2, 3riota2f 6279 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  E!wreu 2809  iota_crio 6256
This theorem is referenced by:  eqsup  7936  fin23lem22  8728  subadd  9846  divmul  10235  uzinfmi  11190  fllelt  11934  flflp1  11944  flval2  11950  flbi  11952  remim  12950  resqrtcl  13087  resqrtthlem  13088  sqrtneg  13101  sqrtthlem  13195  divalgmod  14064  qnumdenbi  14277  catidd  15077  lubprop  15616  glbprop  15629  isglbd  15747  poslubd  15778  ismgmid  15891  isgrpinv  16100  pj1id  16717  coeeq  22624  ismir  24040  mireq  24046  ismidb  24144  islmib  24153  usgraidx2vlem2  24392  nbgraf1olem3  24443  frgrancvvdeqlem4  25033  cmpidelt  25331  cnid  25353  addinv  25354  mulid  25358  hilid  26078  pjpreeq  26316  cnvbraval  27029  cdj3lem2  27354  xdivmul  27621  cvmliftphtlem  28762  cvmlift3lem4  28767  cvmlift3lem6  28769  cvmlift3lem9  28772  transportprops  29684  ltflcei  30043  exidresid  30341  fourierdlem50  31939  usgedgvadf1lem2  32414  usgedgvadf1ALTlem2  32417  lshpkrlem1  34835  cdlemeiota  36311  dochfl1  37203  hgmapvs  37621
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-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-reu 2814  df-v 3111  df-sbc 3328  df-un 3480  df-sn 4030  df-pr 4032  df-uni 4250  df-iota 5556  df-riota 6257
  Copyright terms: Public domain W3C validator