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  11538  sumeq1  12069  sumeq2  12073  zsumdc  12099  isumclim3  12138  isumshft  12205  prodeq1f  12267  prodeq2w  12271  prodeq2  12272  zproddc  12294  pcval  13023  grpidvalg  13640  grpidpropdg  13641  igsumvalx  13656  gsumpropd  13659  gsumpropd2  13660  gsumress  13662  gsumval2  13664  gfsumval  14106  dfur2g  14209  oppr0g  14329  oppr1g  14330