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

Theorem riotabidv 7096
 Description: Formula-building deduction 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 631 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 6309 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 7094 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 7094 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2858 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ℩cio 6282  ℩crio 7093 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4802  df-iota 6284  df-riota 7094 This theorem is referenced by:  riotaeqbidv  7097  csbriota  7109  sup0riota  8916  infval  8937  fin23lem27  9742  subval  10869  divval  11292  flval  13162  ceilval2  13208  cjval  14456  sqrtval  14591  qnumval  16070  qdenval  16071  lubval  17589  glbval  17602  joinval2  17614  meetval2  17628  grpinvval  18140  pj1fval  18816  pj1val  18817  q1pval  24764  coeval  24830  quotval  24898  ismidb  26582  lmif  26589  islmib  26591  uspgredg2v  27024  usgredg2v  27027  frgrncvvdeqlem8  28101  frgrncvvdeqlem9  28102  grpoinvval  28316  pjhval  29190  nmopadjlei  29881  cdj3lem2  30228  cvmliftlem15  32673  cvmlift2lem4  32681  cvmlift2  32691  cvmlift3lem2  32695  cvmlift3lem4  32697  cvmlift3lem6  32699  cvmlift3lem7  32700  cvmlift3lem9  32702  cvmlift3  32703  fvtransport  33621  lshpkrlem1  36425  lshpkrlem2  36426  lshpkrlem3  36427  lshpkrcl  36431  trlset  37476  trlval  37477  cdleme27b  37683  cdleme29b  37690  cdleme31so  37694  cdleme31sn1  37696  cdleme31sn1c  37703  cdleme31fv  37705  cdlemefrs29clN  37714  cdleme40v  37784  cdlemg1cN  37902  cdlemg1cex  37903  cdlemksv  38159  cdlemkuu  38210  cdlemkid3N  38248  cdlemkid4  38249  cdlemm10N  38433  dicval  38491  dihval  38547  dochfl1  38791  lcfl7N  38816  lcfrlem8  38864  lcfrlem9  38865  lcf1o  38866  mapdhval  39039  hvmapval  39075  hvmapvalvalN  39076  hdmap1fval  39111  hdmap1vallem  39112  hdmap1val  39113  hdmap1cbv  39117  hdmapfval  39142  hdmapval  39143  hgmapffval  39200  hgmapfval  39201  hgmapval  39202  resubval  39548  unxpwdom3  40082  mpaaval  40138
 Copyright terms: Public domain W3C validator