Theorem iotabidv 6476

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547  ℩cio 6446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-uni 4846  df-iota 6448

This theorem is referenced by:  csbiota  6485  dffv3  6830  fveq1  6833  fveq2  6834  fvres  6853  csbfv12  6879  opabiota  6916  fvco2  6931  fvopab5  6976  riotaeqdv  7321  riotabidv  7322  riotabidva  7339  erov  8758  iunfictbso  10034  isf32lem9  10281  shftval  15034  sumeq1  15649  sumeq2w  15652  sumeq2ii  15653  sumeq2sdv  15663  zsum  15678  isumclim3  15719  isumshft  15802  prodeq1f  15869  prodeq1  15870  prodeq2w  15873  prodeq2ii  15874  prodeq2sdv  15886  zprod  15900  iprodclim3  15963  pcval  16813  grpidval  18627  grpidpropd  18628  gsumvalx  18642  gsumpropd  18644  gsumpropd2lem  18645  gsumress  18648  psgnfval  19473  psgnval  19480  psgndif  21584  dchrptlem1  27252  lgsdchrval  27342  nosupcbv  27691  nosupfv  27695  noinfcbv  27706  noinffv  27710  ajval  30957  adjval  31986  urpropd  33319  resv1r  33429  opprqus0g  33580  prodeq12sdv  36447  cbvsumdavw  36508  cbvproddavw  36509  cbvsumdavw2  36524  cbvproddavw2  36525  bj-finsumval0  37646  uncov  37969  dfpre2  38845  dfpre3  38846  dfpre4  38848  afv2eq12d  47679  funressndmafv2rn  47687  afv2res  47703  dfafv23  47717  afv2co2  47721