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

Theorem iotabidv 5789
 Description: Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
Hypothesis
Ref Expression
iotabidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
iotabidv (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem iotabidv
StepHypRef Expression
1 iotabidv.1 . . 3 (𝜑 → (𝜓𝜒))
21alrimiv 1842 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 iotabi 5777 . 2 (∀𝑥(𝜓𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒))
42, 3syl 17 1 (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475  ℩cio 5766 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 This theorem is referenced by:  csbiota  5797  dffv3  6099  fveq1  6102  fveq2  6103  fvres  6117  csbfv12  6141  opabiota  6171  fvco2  6183  fvopab5  6217  riotaeqdv  6512  riotabidv  6513  riotabidva  6527  erov  7731  iunfictbso  8820  isf32lem9  9066  shftval  13662  sumeq1  14267  sumeq2w  14270  sumeq2ii  14271  zsum  14296  isumclim3  14332  isumshft  14410  prodeq1f  14477  prodeq2w  14481  prodeq2ii  14482  zprod  14506  iprodclim3  14570  pcval  15387  grpidval  17083  grpidpropd  17084  gsumvalx  17093  gsumpropd  17095  gsumpropd2lem  17096  gsumress  17099  psgnfval  17743  psgnval  17750  psgndif  19767  dchrptlem1  24789  lgsdchrval  24879  ajval  27101  adjval  28133  resv1r  29168  bj-finsumval0  32324  uncov  32560
 Copyright terms: Public domain W3C validator