Theorem iotabidv 6521

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  ℩cio 6491

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871  df-iota 6493

This theorem is used by:  csbiota  6530  dffv3  6878  fveq1  6881  fveq2  6882  fvres  6901  csbfv12  6927  opabiota  6964  fvco2  6979  fvopab5  7024  riotaeqdv  7374  riotabidv  7375  riotabidva  7392  erov  8817  uncov  8875  iunfictbso  10120  isf32lem9  10366  shftval  15149  sumeq1  15778  sumeq2w  15781  sumeq2ii  15782  sumeq2sdv  15792  zsum  15806  isumclim3  15847  isumshft  15930  prodeq1f  15997  prodeq1  15998  prodeq2w  16001  prodeq2ii  16002  prodeq2sdv  16014  zprod  16028  iprodclim3  16091  pcval  16940  grpidval  18758  grpidpropd  18759  gsumvalx  18782  gsumpropd  18784  gsumpropd2lem  18785  gsumress  18788  psgnfval  19631  psgnval  19638  psgndif  21819  dchrptlem1  27501  lgsdchrval  27591  nosupcbv  27939  nosupfv  27943  noinfcbv  27954  noinffv  27958  ajval  31343  adjval  32372  urpropd  33672  resv1r  33781  opprqus0g  33894  prodeq12sdv  36840  cbvsumdavw  36901  cbvproddavw  36902  cbvsumdavw2  36917  cbvproddavw2  36918  bj-finsumval0  38039  dfpre2  39227  dfpre3  39228  dfpre4  39230  afv2eq12d  48105  funressndmafv2rn  48113  afv2res  48129  dfafv23  48143  afv2co2  48147