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

Theorem iotabidv 6082
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 2020 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 iotabi 6070 . 2 (∀𝑥(𝜓𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒))
42, 3syl 17 1 (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1635   = wceq 1637  cio 6059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rex 3101  df-uni 4627  df-iota 6061
This theorem is referenced by:  csbiota  6091  dffv3  6401  fveq1  6404  fveq2  6405  fvres  6424  csbfv12  6448  opabiota  6479  fvco2  6491  fvopab5  6528  riotaeqdv  6833  riotabidv  6834  riotabidva  6848  erov  8077  iunfictbso  9217  isf32lem9  9465  shftval  14033  sumeq1  14638  sumeq2w  14641  sumeq2ii  14642  zsum  14668  isumclim3  14709  isumshft  14789  prodeq1f  14855  prodeq2w  14859  prodeq2ii  14860  zprod  14884  iprodclim3  14947  pcval  15762  grpidval  17461  grpidpropd  17462  gsumvalx  17471  gsumpropd  17473  gsumpropd2lem  17474  gsumress  17477  psgnfval  18117  psgnval  18124  psgndif  20152  dchrptlem1  25199  lgsdchrval  25289  ajval  28042  adjval  29074  resv1r  30159  nosupfv  32170  noeta  32186  bj-finsumval0  33461  uncov  33700  afv2eq12d  41801  funressndmafv2rn  41809  afv2res  41825  dfafv23  41839  afv2co2  41843
  Copyright terms: Public domain W3C validator