Theorem iotabidv 6557

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537  ℩cio 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-iota 6525

This theorem is referenced by:  csbiota  6566  dffv3  6916  fveq1  6919  fveq2  6920  fvres  6939  csbfv12  6968  opabiota  7004  fvco2  7019  fvopab5  7062  riotaeqdv  7405  riotabidv  7406  riotabidva  7424  erov  8872  iunfictbso  10183  isf32lem9  10430  shftval  15123  sumeq1  15737  sumeq2w  15740  sumeq2ii  15741  sumeq2sdv  15751  zsum  15766  isumclim3  15807  isumshft  15887  prodeq1f  15954  prodeq1  15955  prodeq2w  15958  prodeq2ii  15959  prodeq2sdv  15971  zprod  15985  iprodclim3  16048  pcval  16891  grpidval  18699  grpidpropd  18700  gsumvalx  18714  gsumpropd  18716  gsumpropd2lem  18717  gsumress  18720  psgnfval  19542  psgnval  19549  psgndif  21643  dchrptlem1  27326  lgsdchrval  27416  nosupcbv  27765  nosupfv  27769  noinfcbv  27780  noinffv  27784  ajval  30893  adjval  31922  urpropd  33212  resv1r  33333  opprqus0g  33483  prodeq12sdv  36184  cbvsumdavw  36245  cbvproddavw  36246  cbvsumdavw2  36261  cbvproddavw2  36262  bj-finsumval0  37251  uncov  37561  afv2eq12d  47130  funressndmafv2rn  47138  afv2res  47154  dfafv23  47168  afv2co2  47172