Theorem iotabidv 6497

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  ℩cio 6464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3933  df-uni 4874  df-iota 6466

This theorem is referenced by:  csbiota  6506  dffv3  6856  fveq1  6859  fveq2  6860  fvres  6879  csbfv12  6908  opabiota  6945  fvco2  6960  fvopab5  7003  riotaeqdv  7347  riotabidv  7348  riotabidva  7365  erov  8789  iunfictbso  10073  isf32lem9  10320  shftval  15046  sumeq1  15661  sumeq2w  15664  sumeq2ii  15665  sumeq2sdv  15675  zsum  15690  isumclim3  15731  isumshft  15811  prodeq1f  15878  prodeq1  15879  prodeq2w  15882  prodeq2ii  15883  prodeq2sdv  15895  zprod  15909  iprodclim3  15972  pcval  16821  grpidval  18594  grpidpropd  18595  gsumvalx  18609  gsumpropd  18611  gsumpropd2lem  18612  gsumress  18615  psgnfval  19436  psgnval  19443  psgndif  21517  dchrptlem1  27181  lgsdchrval  27271  nosupcbv  27620  nosupfv  27624  noinfcbv  27635  noinffv  27639  ajval  30796  adjval  31825  urpropd  33189  resv1r  33317  opprqus0g  33467  prodeq12sdv  36201  cbvsumdavw  36262  cbvproddavw  36263  cbvsumdavw2  36278  cbvproddavw2  36279  bj-finsumval0  37268  uncov  37590  afv2eq12d  47206  funressndmafv2rn  47214  afv2res  47230  dfafv23  47244  afv2co2  47248