Theorem iotabidv 6522

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569  ℩cio 6492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-iota 6494

This theorem is used by:  csbiota  6531  dffv3  6881  fveq1  6884  fveq2  6885  fvres  6904  csbfv12  6930  opabiota  6967  fvco2  6982  fvopab5  7027  riotaeqdv  7378  riotabidv  7379  riotabidva  7396  erov  8836  uncov  8894  iunfictbso  10194  isf32lem9  10440  shftval  15228  sumeq1  15857  sumeq2w  15860  sumeq2ii  15861  sumeq2sdv  15871  zsum  15885  isumclim3  15926  isumshft  16009  prodeq1f  16076  prodeq1  16077  prodeq2w  16080  prodeq2ii  16081  prodeq2sdv  16092  zprod  16105  iprodclim3  16168  pcval  17023  grpidval  18841  grpidpropd  18843  gsumvalx  18866  gsumpropd  18868  gsumpropd2lem  18869  gsumress  18872  psgnfval  19715  psgnval  19722  psgndif  21909  dchrptlem1  27592  lgsdchrval  27682  nosupcbv  28060  nosupfv  28064  noinfcbv  28075  noinffv  28079  ajval  31464  adjval  32493  urpropd  33834  resv1r  33943  opprqus0g  34057  prodeq12sdv  37082  cbvsumdavw  37143  cbvproddavw  37144  cbvsumdavw2  37159  cbvproddavw2  37160  bj-finsumval0  38282  dfpre2  39485  dfpre3  39486  dfpre4  39488  afv2eq12d  48361  funressndmafv2rn  48369  afv2res  48385  dfafv23  48399  afv2co2  48403