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

Theorem riotabidv 7172
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 632 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 6364 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 7170 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 7170 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2803 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2110  cio 6336  crio 7169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-iota 6338  df-riota 7170
This theorem is referenced by:  riotaeqbidv  7173  csbriota  7186  sup0riota  9081  infval  9102  fin23lem27  9942  subval  11069  divval  11492  flval  13369  ceilval2  13415  cjval  14665  sqrtval  14800  qnumval  16293  qdenval  16294  lubval  17862  glbval  17875  joinval2  17887  meetval2  17901  grpinvval  18408  pj1fval  19084  pj1val  19085  q1pval  25051  coeval  25117  quotval  25185  ismidb  26869  lmif  26876  islmib  26878  uspgredg2v  27312  usgredg2v  27315  frgrncvvdeqlem8  28389  frgrncvvdeqlem9  28390  grpoinvval  28604  pjhval  29478  nmopadjlei  30169  cdj3lem2  30516  cvmliftlem15  32973  cvmlift2lem4  32981  cvmlift2  32991  cvmlift3lem2  32995  cvmlift3lem4  32997  cvmlift3lem6  32999  cvmlift3lem7  33000  cvmlift3lem9  33002  cvmlift3  33003  ttrcltr  33515  fvtransport  34071  lshpkrlem1  36861  lshpkrlem2  36862  lshpkrlem3  36863  lshpkrcl  36867  trlset  37912  trlval  37913  cdleme27b  38119  cdleme29b  38126  cdleme31so  38130  cdleme31sn1  38132  cdleme31sn1c  38139  cdleme31fv  38141  cdlemefrs29clN  38150  cdleme40v  38220  cdlemg1cN  38338  cdlemg1cex  38339  cdlemksv  38595  cdlemkuu  38646  cdlemkid3N  38684  cdlemkid4  38685  cdlemm10N  38869  dicval  38927  dihval  38983  dochfl1  39227  lcfl7N  39252  lcfrlem8  39300  lcfrlem9  39301  lcf1o  39302  mapdhval  39475  hvmapval  39511  hvmapvalvalN  39512  hdmap1fval  39547  hdmap1vallem  39548  hdmap1val  39549  hdmap1cbv  39553  hdmapfval  39578  hdmapval  39579  hgmapffval  39636  hgmapfval  39637  hgmapval  39638  resubval  40058  unxpwdom3  40623  mpaaval  40679
  Copyright terms: Public domain W3C validator