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

Theorem riotabidv 6937
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 619 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 6170 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 6935 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 6935 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2833 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  cio 6147  crio 6934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2744
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-rex 3088  df-uni 4709  df-iota 6149  df-riota 6935
This theorem is referenced by:  riotaeqbidv  6938  csbriota  6947  sup0riota  8722  infval  8743  fin23lem27  9546  subval  10675  divval  11099  flval  12977  ceilval2  13023  cjval  14320  sqrtval  14455  qnumval  15931  qdenval  15932  lubval  17464  glbval  17477  joinval2  17489  meetval2  17503  grpinvval  17943  pj1fval  18590  pj1val  18591  q1pval  24462  coeval  24528  quotval  24596  ismidb  26278  lmif  26285  islmib  26287  uspgredg2v  26721  usgredg2v  26724  frgrncvvdeqlem8  27852  frgrncvvdeqlem9  27853  grpoinvval  28089  pjhval  28967  nmopadjlei  29658  cdj3lem2  30005  cvmliftlem15  32159  cvmlift2lem4  32167  cvmlift2  32177  cvmlift3lem2  32181  cvmlift3lem4  32183  cvmlift3lem6  32185  cvmlift3lem7  32186  cvmlift3lem9  32188  cvmlift3  32189  fvtransport  33043  lshpkrlem1  35720  lshpkrlem2  35721  lshpkrlem3  35722  lshpkrcl  35726  trlset  36771  trlval  36772  cdleme27b  36978  cdleme29b  36985  cdleme31so  36989  cdleme31sn1  36991  cdleme31sn1c  36998  cdleme31fv  37000  cdlemefrs29clN  37009  cdleme40v  37079  cdlemg1cN  37197  cdlemg1cex  37198  cdlemksv  37454  cdlemkuu  37505  cdlemkid3N  37543  cdlemkid4  37544  cdlemm10N  37728  dicval  37786  dihval  37842  dochfl1  38086  lcfl7N  38111  lcfrlem8  38159  lcfrlem9  38160  lcf1o  38161  mapdhval  38334  hvmapval  38370  hvmapvalvalN  38371  hdmap1fval  38406  hdmap1vallem  38407  hdmap1val  38408  hdmap1cbv  38412  hdmapfval  38437  hdmapval  38438  hgmapffval  38495  hgmapfval  38496  hgmapval  38497  resubval  38658  unxpwdom3  39120  mpaaval  39176
  Copyright terms: Public domain W3C validator