Theorem iotabidv 6517

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-iota 6489

This theorem is used by:  csbiota  6526  dffv3  6875  fveq1  6878  fveq2  6879  fvres  6898  csbfv12  6924  opabiota  6961  fvco2  6976  fvopab5  7021  riotaeqdv  7372  riotabidv  7373  riotabidva  7390  erov  8815  uncov  8873  iunfictbso  10118  isf32lem9  10364  shftval  15148  sumeq1  15777  sumeq2w  15780  sumeq2ii  15781  sumeq2sdv  15791  zsum  15805  isumclim3  15846  isumshft  15929  prodeq1f  15996  prodeq1  15997  prodeq2w  16000  prodeq2ii  16001  prodeq2sdv  16012  zprod  16025  iprodclim3  16088  pcval  16937  grpidval  18755  grpidpropd  18756  gsumvalx  18779  gsumpropd  18781  gsumpropd2lem  18782  gsumress  18785  psgnfval  19628  psgnval  19635  psgndif  21816  dchrptlem1  27501  lgsdchrval  27591  nosupcbv  27939  nosupfv  27943  noinfcbv  27954  noinffv  27958  ajval  31343  adjval  32372  urpropd  33671  resv1r  33780  opprqus0g  33893  prodeq12sdv  36839  cbvsumdavw  36900  cbvproddavw  36901  cbvsumdavw2  36916  cbvproddavw2  36917  bj-finsumval0  38038  dfpre2  39226  dfpre3  39227  dfpre4  39229  afv2eq12d  48104  funressndmafv2rn  48112  afv2res  48128  dfafv23  48142  afv2co2  48146