Theorem iotabidv 5242

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1362   = wceq 1364  ℩cio 5218

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3841  df-iota 5220

This theorem is referenced by:  csbiotag  5252  dffv3g  5557  fveq1  5560  fveq2  5561  fvres  5585  csbfv12g  5599  fvco2  5633  riotaeqdv  5881  riotabidv  5882  riotabidva  5897  ovtposg  6326  shftval  11009  sumeq1  11539  sumeq2  11543  zsumdc  11568  isumclim3  11607  isumshft  11674  prodeq1f  11736  prodeq2w  11740  prodeq2  11741  zproddc  11763  pcval  12492  grpidvalg  13077  grpidpropdg  13078  igsumvalx  13093  gsumpropd  13096  gsumpropd2  13097  gsumress  13099  gsumval2  13101  dfur2g  13596  oppr0g  13715  oppr1g  13716