Theorem iotabidv 6471

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541  ℩cio 6441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4859  df-iota 6443

This theorem is referenced by:  csbiota  6480  dffv3  6824  fveq1  6827  fveq2  6828  fvres  6847  csbfv12  6873  opabiota  6910  fvco2  6925  fvopab5  6968  riotaeqdv  7310  riotabidv  7311  riotabidva  7328  erov  8744  iunfictbso  10011  isf32lem9  10258  shftval  14987  sumeq1  15602  sumeq2w  15605  sumeq2ii  15606  sumeq2sdv  15616  zsum  15631  isumclim3  15672  isumshft  15752  prodeq1f  15819  prodeq1  15820  prodeq2w  15823  prodeq2ii  15824  prodeq2sdv  15836  zprod  15850  iprodclim3  15913  pcval  16762  grpidval  18575  grpidpropd  18576  gsumvalx  18590  gsumpropd  18592  gsumpropd2lem  18593  gsumress  18596  psgnfval  19418  psgnval  19425  psgndif  21545  dchrptlem1  27208  lgsdchrval  27298  nosupcbv  27647  nosupfv  27651  noinfcbv  27662  noinffv  27666  ajval  30848  adjval  31877  urpropd  33206  resv1r  33311  opprqus0g  33462  prodeq12sdv  36269  cbvsumdavw  36330  cbvproddavw  36331  cbvsumdavw2  36346  cbvproddavw2  36347  bj-finsumval0  37336  uncov  37647  dfpre2  38496  dfpre3  38497  dfpre4  38499  afv2eq12d  47320  funressndmafv2rn  47328  afv2res  47344  dfafv23  47358  afv2co2  47362