Theorem iotabidv 6527

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-iota 6495

This theorem is referenced by:  csbiota  6536  dffv3  6887  fveq1  6890  fveq2  6891  fvres  6910  csbfv12  6939  opabiota  6974  fvco2  6988  fvopab5  7030  riotaeqdv  7365  riotabidv  7366  riotabidva  7384  erov  8807  iunfictbso  10108  isf32lem9  10355  shftval  15020  sumeq1  15634  sumeq2w  15637  sumeq2ii  15638  zsum  15663  isumclim3  15704  isumshft  15784  prodeq1f  15851  prodeq2w  15855  prodeq2ii  15856  zprod  15880  iprodclim3  15943  pcval  16776  grpidval  18579  grpidpropd  18580  gsumvalx  18594  gsumpropd  18596  gsumpropd2lem  18597  gsumress  18600  psgnfval  19367  psgnval  19374  psgndif  21154  dchrptlem1  26764  lgsdchrval  26854  nosupcbv  27202  nosupfv  27206  noinfcbv  27217  noinffv  27221  ajval  30109  adjval  31138  urpropd  32373  resv1r  32451  opprqus0g  32599  bj-finsumval0  36161  uncov  36464  afv2eq12d  45913  funressndmafv2rn  45921  afv2res  45937  dfafv23  45951  afv2co2  45955