Theorem iotabidv 5872

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

Step	Hyp	Ref	Expression
1		iotabidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alrimiv 1855	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		iotabi 5860	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481   = wceq 1483  ℩cio 5849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-iota 5851

This theorem is referenced by:  csbiota  5881  dffv3  6187  fveq1  6190  fveq2  6191  fvres  6207  csbfv12  6231  opabiota  6261  fvco2  6273  fvopab5  6309  riotaeqdv  6612  riotabidv  6613  riotabidva  6627  erov  7844  iunfictbso  8937  isf32lem9  9183  shftval  13814  sumeq1  14419  sumeq2w  14422  sumeq2ii  14423  zsum  14449  isumclim3  14490  isumshft  14571  prodeq1f  14638  prodeq2w  14642  prodeq2ii  14643  zprod  14667  iprodclim3  14731  pcval  15549  grpidval  17260  grpidpropd  17261  gsumvalx  17270  gsumpropd  17272  gsumpropd2lem  17273  gsumress  17276  psgnfval  17920  psgnval  17927  psgndif  19948  dchrptlem1  24989  lgsdchrval  25079  ajval  27717  adjval  28749  resv1r  29837  nosupfv  31852  noeta  31868  bj-finsumval0  33147  uncov  33390