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

Theorem iotabidv 5775
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 5763 . 2 (∀𝑥(𝜓𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒))
42, 3syl 17 1 (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wal 1473   = wceq 1475  cio 5752
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 4368  df-iota 5754
This theorem is referenced by:  csbiota  5783  dffv3  6084  fveq1  6087  fveq2  6088  fvres  6102  csbfv12  6126  opabiota  6156  fvco2  6168  fvopab5  6202  riotaeqdv  6490  riotabidv  6491  riotabidva  6505  erov  7709  iunfictbso  8798  isf32lem9  9044  shftval  13611  sumeq1  14216  sumeq2w  14219  sumeq2ii  14220  zsum  14245  isumclim3  14281  isumshft  14359  prodeq1f  14426  prodeq2w  14430  prodeq2ii  14431  zprod  14455  iprodclim3  14519  pcval  15336  grpidval  17032  grpidpropd  17033  gsumvalx  17042  gsumpropd  17044  gsumpropd2lem  17045  gsumress  17048  psgnfval  17692  psgnval  17699  psgndif  19715  dchrptlem1  24734  lgsdchrval  24824  ajval  26895  adjval  27927  resv1r  28962  bj-finsumval0  32118  uncov  32354
  Copyright terms: Public domain W3C validator