Theorem iotabidv 6511

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  ℩cio 6481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-uni 4867  df-iota 6483

This theorem is used by:  csbiota  6520  dffv3  6869  fveq1  6872  fveq2  6873  fvres  6892  csbfv12  6918  opabiota  6955  fvco2  6970  fvopab5  7015  riotaeqdv  7366  riotabidv  7367  riotabidva  7384  erov  8813  uncov  8871  iunfictbso  10165  isf32lem9  10411  shftval  15195  sumeq1  15824  sumeq2w  15827  sumeq2ii  15828  sumeq2sdv  15838  zsum  15852  isumclim3  15893  isumshft  15976  prodeq1f  16043  prodeq1  16044  prodeq2w  16047  prodeq2ii  16048  prodeq2sdv  16059  zprod  16072  iprodclim3  16135  pcval  16984  grpidval  18802  grpidpropd  18804  gsumvalx  18827  gsumpropd  18829  gsumpropd2lem  18830  gsumress  18833  psgnfval  19676  psgnval  19683  psgndif  21870  dchrptlem1  27555  lgsdchrval  27645  nosupcbv  27993  nosupfv  27997  noinfcbv  28008  noinffv  28012  ajval  31397  adjval  32426  urpropd  33725  resv1r  33834  opprqus0g  33948  prodeq12sdv  36929  cbvsumdavw  36990  cbvproddavw  36991  cbvsumdavw2  37006  cbvproddavw2  37007  bj-finsumval0  38126  dfpre2  39329  dfpre3  39330  dfpre4  39332  afv2eq12d  48207  funressndmafv2rn  48215  afv2res  48231  dfafv23  48245  afv2co2  48249