Theorem iotabidv 6320

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1537   = wceq 1539  ℩cio 6293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-ss 3876  df-uni 4800  df-iota 6295

This theorem is referenced by:  csbiota  6329  dffv3  6655  fveq1  6658  fveq2  6659  fvres  6678  csbfv12  6702  opabiota  6736  fvco2  6750  fvopab5  6792  riotaeqdv  7110  riotabidv  7111  riotabidva  7128  erov  8405  iunfictbso  9567  isf32lem9  9814  shftval  14474  sumeq1  15086  sumeq2w  15090  sumeq2ii  15091  zsum  15116  isumclim3  15155  isumshft  15235  prodeq1f  15303  prodeq2w  15307  prodeq2ii  15308  zprod  15332  iprodclim3  15395  pcval  16229  grpidval  17930  grpidpropd  17931  gsumvalx  17945  gsumpropd  17947  gsumpropd2lem  17948  gsumress  17951  psgnfval  18688  psgnval  18695  psgndif  20360  dchrptlem1  25940  lgsdchrval  26030  ajval  28736  adjval  29765  resv1r  31055  nosupcbv  33463  nosupfv  33467  noinfcbv  33478  noinffv  33482  bj-finsumval0  34973  uncov  35311  afv2eq12d  44132  funressndmafv2rn  44140  afv2res  44156  dfafv23  44170  afv2co2  44174