Theorem iotabidv 6202

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

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1518   = wceq 1520  ℩cio 6179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-rex 3109  df-uni 4740  df-iota 6181

This theorem is referenced by:  csbiota  6210  dffv3  6526  fveq1  6529  fveq2  6530  fvres  6549  csbfv12  6573  opabiota  6605  fvco2  6617  fvopab5  6656  riotaeqdv  6969  riotabidv  6970  riotabidva  6984  erov  8235  iunfictbso  9375  isf32lem9  9618  shftval  14255  sumeq1  14867  sumeq2w  14870  sumeq2ii  14871  zsum  14896  isumclim3  14935  isumshft  15015  prodeq1f  15083  prodeq2w  15087  prodeq2ii  15088  zprod  15112  iprodclim3  15175  pcval  15998  grpidval  17687  grpidpropd  17688  gsumvalx  17697  gsumpropd  17699  gsumpropd2lem  17700  gsumress  17703  psgnfval  18347  psgnval  18354  psgndif  20416  dchrptlem1  25510  lgsdchrval  25600  ajval  28317  adjval  29346  resv1r  30519  nosupfv  32760  noeta  32776  bj-finsumval0  34065  uncov  34350  afv2eq12d  42884  funressndmafv2rn  42892  afv2res  42908  dfafv23  42922  afv2co2  42926