Theorem iotabidv 6531

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531   = wceq 1533  ℩cio 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-ss 3962  df-uni 4909  df-iota 6499

This theorem is referenced by:  csbiota  6540  dffv3  6890  fveq1  6893  fveq2  6894  fvres  6913  csbfv12  6942  opabiota  6978  fvco2  6992  fvopab5  7035  riotaeqdv  7374  riotabidv  7375  riotabidva  7393  erov  8831  iunfictbso  10137  isf32lem9  10384  shftval  15054  sumeq1  15668  sumeq2w  15671  sumeq2ii  15672  zsum  15697  isumclim3  15738  isumshft  15818  prodeq1f  15885  prodeq2w  15889  prodeq2ii  15890  zprod  15914  iprodclim3  15977  pcval  16813  grpidval  18621  grpidpropd  18622  gsumvalx  18636  gsumpropd  18638  gsumpropd2lem  18639  gsumress  18642  psgnfval  19460  psgnval  19467  psgndif  21539  dchrptlem1  27228  lgsdchrval  27318  nosupcbv  27666  nosupfv  27670  noinfcbv  27681  noinffv  27685  ajval  30728  adjval  31757  urpropd  33007  resv1r  33124  opprqus0g  33275  bj-finsumval0  36851  uncov  37161  afv2eq12d  46675  funressndmafv2rn  46683  afv2res  46699  dfafv23  46713  afv2co2  46717