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

Theorem iotabidv 6485
Description: Formula-building deduction 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 1931 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 iotabi 6467 . 2 (∀𝑥(𝜓𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒))
42, 3syl 17 1 (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540   = wceq 1542  cio 6451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-uni 4871  df-iota 6453
This theorem is referenced by:  csbiota  6494  dffv3  6843  fveq1  6846  fveq2  6847  fvres  6866  csbfv12  6895  opabiota  6929  fvco2  6943  fvopab5  6985  riotaeqdv  7319  riotabidv  7320  riotabidva  7338  erov  8760  iunfictbso  10057  isf32lem9  10304  shftval  14966  sumeq1  15580  sumeq2w  15584  sumeq2ii  15585  zsum  15610  isumclim3  15651  isumshft  15731  prodeq1f  15798  prodeq2w  15802  prodeq2ii  15803  zprod  15827  iprodclim3  15890  pcval  16723  grpidval  18523  grpidpropd  18524  gsumvalx  18538  gsumpropd  18540  gsumpropd2lem  18541  gsumress  18544  psgnfval  19289  psgnval  19296  psgndif  21022  dchrptlem1  26628  lgsdchrval  26718  nosupcbv  27066  nosupfv  27070  noinfcbv  27081  noinffv  27085  ajval  29845  adjval  30874  resv1r  32173  bj-finsumval0  35785  uncov  36088  afv2eq12d  45521  funressndmafv2rn  45529  afv2res  45545  dfafv23  45559  afv2co2  45563
  Copyright terms: Public domain W3C validator