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

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

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