MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  riotabidv Structured version   Visualization version   GIF version

Theorem riotabidv 6598
Description: Formula-building deduction rule for restricted iota. (Contributed by NM, 15-Sep-2011.)
Hypothesis
Ref Expression
riotabidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
riotabidv (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem riotabidv
StepHypRef Expression
1 riotabidv.1 . . . 4 (𝜑 → (𝜓𝜒))
21anbi2d 739 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 5860 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 6596 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 6596 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2679 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  cio 5837  crio 6595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-uni 4428  df-iota 5839  df-riota 6596
This theorem is referenced by:  riotaeqbidv  6599  csbriota  6608  sup0riota  8356  infval  8377  fin23lem27  9135  subval  10257  divval  10672  flval  12578  ceilval2  12624  cjval  13823  sqrtval  13958  qnumval  15426  qdenval  15427  lubval  16965  glbval  16978  joinval2  16990  meetval2  17004  grpinvval  17442  pj1fval  18088  pj1val  18089  q1pval  23894  coeval  23960  quotval  24028  ismidb  25651  lmif  25658  islmib  25660  uspgredg2v  26097  usgredg2v  26100  frgrncvvdeqlem8  27150  frgrncvvdeqlem9  27151  grpoinvval  27347  pjhval  28226  nmopadjlei  28917  cdj3lem2  29264  cvmliftlem15  31254  cvmlift2lem4  31262  cvmlift2  31272  cvmlift3lem2  31276  cvmlift3lem4  31278  cvmlift3lem6  31280  cvmlift3lem7  31281  cvmlift3lem9  31283  cvmlift3  31284  fvtransport  32114  lshpkrlem1  34216  lshpkrlem2  34217  lshpkrlem3  34218  lshpkrcl  34222  trlset  35267  trlval  35268  cdleme27b  35475  cdleme29b  35482  cdleme31so  35486  cdleme31sn1  35488  cdleme31sn1c  35495  cdleme31fv  35497  cdlemefrs29clN  35506  cdleme40v  35576  cdlemg1cN  35694  cdlemg1cex  35695  cdlemksv  35951  cdlemkuu  36002  cdlemkid3N  36040  cdlemkid4  36041  cdlemm10N  36226  dicval  36284  dihval  36340  dochfl1  36584  lcfl7N  36609  lcfrlem8  36657  lcfrlem9  36658  lcf1o  36659  mapdhval  36832  hvmapval  36868  hvmapvalvalN  36869  hdmap1fval  36905  hdmap1vallem  36906  hdmap1val  36907  hdmap1cbv  36911  hdmapfval  36938  hdmapval  36939  hgmapffval  36996  hgmapfval  36997  hgmapval  36998  unxpwdom3  37484  mpaaval  37540
  Copyright terms: Public domain W3C validator