Theorem iotabidv 5309

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1395   = wceq 1397  ℩cio 5284

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-iota 5286

This theorem is referenced by:  csbiotag  5319  dffv3g  5635  fveq1  5638  fveq2  5639  fvres  5663  csbfv12g  5679  fvco2  5715  riotaeqdv  5972  riotabidv  5973  riotabidva  5989  ovtposg  6425  shftval  11387  sumeq1  11917  sumeq2  11921  zsumdc  11947  isumclim3  11986  isumshft  12053  prodeq1f  12115  prodeq2w  12119  prodeq2  12120  zproddc  12142  pcval  12871  grpidvalg  13458  grpidpropdg  13459  igsumvalx  13474  gsumpropd  13477  gsumpropd2  13478  gsumress  13480  gsumval2  13482  dfur2g  13978  oppr0g  14097  oppr1g  14098  gfsumval  16697