Theorem iotabidv 6483

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542  ℩cio 6453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-iota 6455

This theorem is referenced by:  csbiota  6492  dffv3  6837  fveq1  6840  fveq2  6841  fvres  6860  csbfv12  6886  opabiota  6923  fvco2  6938  fvopab5  6982  riotaeqdv  7325  riotabidv  7326  riotabidva  7343  erov  8761  iunfictbso  10036  isf32lem9  10283  shftval  15036  sumeq1  15651  sumeq2w  15654  sumeq2ii  15655  sumeq2sdv  15665  zsum  15680  isumclim3  15721  isumshft  15804  prodeq1f  15871  prodeq1  15872  prodeq2w  15875  prodeq2ii  15876  prodeq2sdv  15888  zprod  15902  iprodclim3  15965  pcval  16815  grpidval  18629  grpidpropd  18630  gsumvalx  18644  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  psgnfval  19475  psgnval  19482  psgndif  21582  dchrptlem1  27227  lgsdchrval  27317  nosupcbv  27666  nosupfv  27670  noinfcbv  27681  noinffv  27685  ajval  30932  adjval  31961  urpropd  33292  resv1r  33399  opprqus0g  33550  prodeq12sdv  36400  cbvsumdavw  36461  cbvproddavw  36462  cbvsumdavw2  36477  cbvproddavw2  36478  bj-finsumval0  37599  uncov  37922  dfpre2  38798  dfpre3  38799  dfpre4  38801  afv2eq12d  47657  funressndmafv2rn  47665  afv2res  47681  dfafv23  47695  afv2co2  47699