Theorem iotabidv 6528

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540   = wceq 1542  ℩cio 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-iota 6496

This theorem is referenced by:  csbiota  6537  dffv3  6888  fveq1  6891  fveq2  6892  fvres  6911  csbfv12  6940  opabiota  6975  fvco2  6989  fvopab5  7031  riotaeqdv  7366  riotabidv  7367  riotabidva  7385  erov  8808  iunfictbso  10109  isf32lem9  10356  shftval  15021  sumeq1  15635  sumeq2w  15638  sumeq2ii  15639  zsum  15664  isumclim3  15705  isumshft  15785  prodeq1f  15852  prodeq2w  15856  prodeq2ii  15857  zprod  15881  iprodclim3  15944  pcval  16777  grpidval  18580  grpidpropd  18581  gsumvalx  18595  gsumpropd  18597  gsumpropd2lem  18598  gsumress  18601  psgnfval  19368  psgnval  19375  psgndif  21155  dchrptlem1  26767  lgsdchrval  26857  nosupcbv  27205  nosupfv  27209  noinfcbv  27220  noinffv  27224  ajval  30114  adjval  31143  urpropd  32378  resv1r  32456  opprqus0g  32604  bj-finsumval0  36166  uncov  36469  afv2eq12d  45923  funressndmafv2rn  45931  afv2res  45947  dfafv23  45961  afv2co2  45965