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

Theorem riotabidv 6567
 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 5831 . 2 (𝜑 → (℩𝑥(𝑥𝐴𝜓)) = (℩𝑥(𝑥𝐴𝜒)))
4 df-riota 6565 . 2 (𝑥𝐴 𝜓) = (℩𝑥(𝑥𝐴𝜓))
5 df-riota 6565 . 2 (𝑥𝐴 𝜒) = (℩𝑥(𝑥𝐴𝜒))
63, 4, 53eqtr4g 2680 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ℩cio 5808  ℩crio 6564 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-uni 4403  df-iota 5810  df-riota 6565 This theorem is referenced by:  riotaeqbidv  6568  csbriota  6577  sup0riota  8315  infval  8336  fin23lem27  9094  subval  10216  divval  10631  flval  12535  ceilval2  12581  cjval  13776  sqrtval  13911  qnumval  15369  qdenval  15370  lubval  16905  glbval  16918  joinval2  16930  meetval2  16944  grpinvval  17382  pj1fval  18028  pj1val  18029  q1pval  23817  coeval  23883  quotval  23951  ismidb  25570  lmif  25577  islmib  25579  uspgredg2v  26009  usgredg2v  26012  frgrncvvdeqlemB  27035  frgrncvvdeqlemC  27036  grpoinvval  27226  pjhval  28105  nmopadjlei  28796  cdj3lem2  29143  cvmliftlem15  30988  cvmlift2lem4  30996  cvmlift2  31006  cvmlift3lem2  31010  cvmlift3lem4  31012  cvmlift3lem6  31014  cvmlift3lem7  31015  cvmlift3lem9  31017  cvmlift3  31018  fvtransport  31781  lshpkrlem1  33877  lshpkrlem2  33878  lshpkrlem3  33879  lshpkrcl  33883  trlset  34928  trlval  34929  cdleme27b  35136  cdleme29b  35143  cdleme31so  35147  cdleme31sn1  35149  cdleme31sn1c  35156  cdleme31fv  35158  cdlemefrs29clN  35167  cdleme40v  35237  cdlemg1cN  35355  cdlemg1cex  35356  cdlemksv  35612  cdlemkuu  35663  cdlemkid3N  35701  cdlemkid4  35702  cdlemm10N  35887  dicval  35945  dihval  36001  dochfl1  36245  lcfl7N  36270  lcfrlem8  36318  lcfrlem9  36319  lcf1o  36320  mapdhval  36493  hvmapval  36529  hvmapvalvalN  36530  hdmap1fval  36566  hdmap1vallem  36567  hdmap1val  36568  hdmap1cbv  36572  hdmapfval  36599  hdmapval  36600  hgmapffval  36657  hgmapfval  36658  hgmapval  36659  unxpwdom3  37145  mpaaval  37202
 Copyright terms: Public domain W3C validator