Theorem iotabidv 5277

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1373   = wceq 1375  ℩cio 5252

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rex 2494  df-uni 3868  df-iota 5254

This theorem is referenced by:  csbiotag  5287  dffv3g  5599  fveq1  5602  fveq2  5603  fvres  5627  csbfv12g  5641  fvco2  5676  riotaeqdv  5928  riotabidv  5929  riotabidva  5945  ovtposg  6375  shftval  11302  sumeq1  11832  sumeq2  11836  zsumdc  11861  isumclim3  11900  isumshft  11967  prodeq1f  12029  prodeq2w  12033  prodeq2  12034  zproddc  12056  pcval  12785  grpidvalg  13372  grpidpropdg  13373  igsumvalx  13388  gsumpropd  13391  gsumpropd2  13392  gsumress  13394  gsumval2  13396  dfur2g  13891  oppr0g  14010  oppr1g  14011