Theorem iotabidv 5340

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1396   = wceq 1398  ℩cio 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3920  df-iota 5317

This theorem is referenced by:  csbiotag  5350  dffv3g  5671  fveq1  5674  fveq2  5675  fvres  5699  csbfv12g  5715  fvco2  5751  riotaeqdv  6012  riotabidv  6013  riotabidva  6029  ovtposg  6503  shftval  11535  sumeq1  12065  sumeq2  12069  zsumdc  12095  isumclim3  12134  isumshft  12201  prodeq1f  12263  prodeq2w  12267  prodeq2  12268  zproddc  12290  pcval  13019  grpidvalg  13670  grpidpropdg  13671  igsumvalx  13686  gsumpropd  13689  gsumpropd2  13690  gsumress  13692  gsumval2  13694  dfur2g  14190  oppr0g  14310  oppr1g  14311  gfsumval  16974