Theorem iotabidv 6509

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561   = wceq 1563  ℩cio 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-uni 4869  df-iota 6481

This theorem is referenced by:  csbiota  6518  dffv3  6867  fveq1  6870  fveq2  6871  fvres  6890  csbfv12  6916  opabiota  6953  fvco2  6968  fvopab5  7013  riotaeqdv  7358  riotabidv  7359  riotabidva  7376  erov  8800  iunfictbso  10086  isf32lem9  10333  shftval  15101  sumeq1  15730  sumeq2w  15733  sumeq2ii  15734  sumeq2sdv  15744  zsum  15759  isumclim3  15800  isumshft  15883  prodeq1f  15950  prodeq1  15951  prodeq2w  15954  prodeq2ii  15955  prodeq2sdv  15967  zprod  15981  iprodclim3  16044  pcval  16894  grpidval  18709  grpidpropd  18710  gsumvalx  18724  gsumpropd  18726  gsumpropd2lem  18727  gsumress  18730  psgnfval  19561  psgnval  19568  psgndif  21712  dchrptlem1  27386  lgsdchrval  27476  nosupcbv  27824  nosupfv  27828  noinfcbv  27839  noinffv  27843  ajval  31122  adjval  32151  urpropd  33463  resv1r  33574  opprqus0g  33689  prodeq12sdv  36591  cbvsumdavw  36652  cbvproddavw  36653  cbvsumdavw2  36668  cbvproddavw2  36669  bj-finsumval0  37789  uncov  38112  dfpre2  38988  dfpre3  38989  dfpre4  38991  afv2eq12d  47807  funressndmafv2rn  47815  afv2res  47831  dfafv23  47845  afv2co2  47849