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  15053  sumeq1  15667  sumeq2w  15670  sumeq2ii  15671  zsum  15696  isumclim3  15737  isumshft  15817  prodeq1f  15884  prodeq2w  15888  prodeq2ii  15889  zprod  15913  iprodclim3  15976  pcval  16812  grpidval  18620  grpidpropd  18621  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  psgnfval  19459  psgnval  19466  psgndif  21538  dchrptlem1  27227  lgsdchrval  27317  nosupcbv  27665  nosupfv  27669  noinfcbv  27680  noinffv  27684  ajval  30727  adjval  31756  urpropd  32996  resv1r  33113  opprqus0g  33263  bj-finsumval0  36834  uncov  37144  afv2eq12d  46658  funressndmafv2rn  46666  afv2res  46682  dfafv23  46696  afv2co2  46700