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

Theorem riotabidv 6513
 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 736 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32iotabidv 5789 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 6511 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 6511 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2669 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ℩cio 5766  ℩crio 6510 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373  df-iota 5768  df-riota 6511 This theorem is referenced by:  riotaeqbidv  6514  csbriota  6523  sup0riota  8254  infval  8275  fin23lem27  9033  subval  10151  divval  10566  flval  12457  ceilval2  12503  cjval  13690  sqrtval  13825  qnumval  15283  qdenval  15284  lubval  16807  glbval  16820  joinval2  16832  meetval2  16846  grpinvval  17284  pj1fval  17930  pj1val  17931  q1pval  23717  coeval  23783  quotval  23851  ismidb  25470  lmif  25477  islmib  25479  usgraidx2v  25922  nbgraf1olem4  25973  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  grpoinvval  26761  pjhval  27640  nmopadjlei  28331  cdj3lem2  28678  cvmliftlem15  30534  cvmlift2lem4  30542  cvmlift2  30552  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  cvmlift3  30564  fvtransport  31309  lshpkrlem1  33415  lshpkrlem2  33416  lshpkrlem3  33417  lshpkrcl  33421  trlset  34466  trlval  34467  cdleme27b  34674  cdleme29b  34681  cdleme31so  34685  cdleme31sn1  34687  cdleme31sn1c  34694  cdleme31fv  34696  cdlemefrs29clN  34705  cdleme40v  34775  cdlemg1cN  34893  cdlemg1cex  34894  cdlemksv  35150  cdlemkuu  35201  cdlemkid3N  35239  cdlemkid4  35240  cdlemm10N  35425  dicval  35483  dihval  35539  dochfl1  35783  lcfl7N  35808  lcfrlem8  35856  lcfrlem9  35857  lcf1o  35858  mapdhval  36031  hvmapval  36067  hvmapvalvalN  36068  hdmap1fval  36104  hdmap1vallem  36105  hdmap1val  36106  hdmap1cbv  36110  hdmapfval  36137  hdmapval  36138  hgmapffval  36195  hgmapfval  36196  hgmapval  36197  unxpwdom3  36683  mpaaval  36740  uspgredg2v  40451  usgredg2v  40454  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478
 Copyright terms: Public domain W3C validator