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  11390  sumeq1  11920  sumeq2  11924  zsumdc  11950  isumclim3  11989  isumshft  12056  prodeq1f  12118  prodeq2w  12122  prodeq2  12123  zproddc  12145  pcval  12874  grpidvalg  13461  grpidpropdg  13462  igsumvalx  13477  gsumpropd  13480  gsumpropd2  13481  gsumress  13483  gsumval2  13485  dfur2g  13981  oppr0g  14100  oppr1g  14101  gfsumval  16706