Theorem iotabidv 6526

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 1928	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		iotabi 6508	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ℩cio 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-iota 6494

This theorem is referenced by:  csbiota  6535  dffv3  6886  fveq1  6889  fveq2  6890  fvres  6909  csbfv12  6938  opabiota  6973  fvco2  6987  fvopab5  7029  riotaeqdv  7368  riotabidv  7369  riotabidva  7387  erov  8810  iunfictbso  10111  isf32lem9  10358  shftval  15025  sumeq1  15639  sumeq2w  15642  sumeq2ii  15643  zsum  15668  isumclim3  15709  isumshft  15789  prodeq1f  15856  prodeq2w  15860  prodeq2ii  15861  zprod  15885  iprodclim3  15948  pcval  16781  grpidval  18586  grpidpropd  18587  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  psgnfval  19409  psgnval  19416  psgndif  21374  dchrptlem1  27003  lgsdchrval  27093  nosupcbv  27441  nosupfv  27445  noinfcbv  27456  noinffv  27460  ajval  30381  adjval  31410  urpropd  32648  resv1r  32726  opprqus0g  32878  bj-finsumval0  36469  uncov  36772  afv2eq12d  46221  funressndmafv2rn  46229  afv2res  46245  dfafv23  46259  afv2co2  46263