Theorem iotabidv 6402

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-iota 6376

This theorem is referenced by:  csbiota  6411  dffv3  6752  fveq1  6755  fveq2  6756  fvres  6775  csbfv12  6799  opabiota  6833  fvco2  6847  fvopab5  6889  riotaeqdv  7213  riotabidv  7214  riotabidva  7232  erov  8561  iunfictbso  9801  isf32lem9  10048  shftval  14713  sumeq1  15328  sumeq2w  15332  sumeq2ii  15333  zsum  15358  isumclim3  15399  isumshft  15479  prodeq1f  15546  prodeq2w  15550  prodeq2ii  15551  zprod  15575  iprodclim3  15638  pcval  16473  grpidval  18260  grpidpropd  18261  gsumvalx  18275  gsumpropd  18277  gsumpropd2lem  18278  gsumress  18281  psgnfval  19023  psgnval  19030  psgndif  20719  dchrptlem1  26317  lgsdchrval  26407  ajval  29124  adjval  30153  resv1r  31443  nosupcbv  33832  nosupfv  33836  noinfcbv  33847  noinffv  33851  bj-finsumval0  35383  uncov  35685  afv2eq12d  44594  funressndmafv2rn  44602  afv2res  44618  dfafv23  44632  afv2co2  44636