Theorem iotabidv 6495

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  ℩cio 6462

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872  df-iota 6464

This theorem is referenced by:  csbiota  6504  dffv3  6854  fveq1  6857  fveq2  6858  fvres  6877  csbfv12  6906  opabiota  6943  fvco2  6958  fvopab5  7001  riotaeqdv  7345  riotabidv  7346  riotabidva  7363  erov  8787  iunfictbso  10067  isf32lem9  10314  shftval  15040  sumeq1  15655  sumeq2w  15658  sumeq2ii  15659  sumeq2sdv  15669  zsum  15684  isumclim3  15725  isumshft  15805  prodeq1f  15872  prodeq1  15873  prodeq2w  15876  prodeq2ii  15877  prodeq2sdv  15889  zprod  15903  iprodclim3  15966  pcval  16815  grpidval  18588  grpidpropd  18589  gsumvalx  18603  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  psgnfval  19430  psgnval  19437  psgndif  21511  dchrptlem1  27175  lgsdchrval  27265  nosupcbv  27614  nosupfv  27618  noinfcbv  27629  noinffv  27633  ajval  30790  adjval  31819  urpropd  33183  resv1r  33311  opprqus0g  33461  prodeq12sdv  36206  cbvsumdavw  36267  cbvproddavw  36268  cbvsumdavw2  36283  cbvproddavw2  36284  bj-finsumval0  37273  uncov  37595  afv2eq12d  47216  funressndmafv2rn  47224  afv2res  47240  dfafv23  47254  afv2co2  47258