Theorem iotabidv 6474

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-iota 6446

This theorem is referenced by:  csbiota  6483  dffv3  6828  fveq1  6831  fveq2  6832  fvres  6851  csbfv12  6877  opabiota  6914  fvco2  6929  fvopab5  6973  riotaeqdv  7316  riotabidv  7317  riotabidva  7334  erov  8752  iunfictbso  10025  isf32lem9  10272  shftval  14998  sumeq1  15613  sumeq2w  15616  sumeq2ii  15617  sumeq2sdv  15627  zsum  15642  isumclim3  15683  isumshft  15763  prodeq1f  15830  prodeq1  15831  prodeq2w  15834  prodeq2ii  15835  prodeq2sdv  15847  zprod  15861  iprodclim3  15924  pcval  16773  grpidval  18587  grpidpropd  18588  gsumvalx  18602  gsumpropd  18604  gsumpropd2lem  18605  gsumress  18608  psgnfval  19433  psgnval  19440  psgndif  21559  dchrptlem1  27215  lgsdchrval  27305  nosupcbv  27654  nosupfv  27658  noinfcbv  27669  noinffv  27673  ajval  30921  adjval  31950  urpropd  33297  resv1r  33404  opprqus0g  33555  prodeq12sdv  36406  cbvsumdavw  36467  cbvproddavw  36468  cbvsumdavw2  36483  cbvproddavw2  36484  bj-finsumval0  37597  uncov  37913  dfpre2  38789  dfpre3  38790  dfpre4  38792  afv2eq12d  47649  funressndmafv2rn  47657  afv2res  47673  dfafv23  47687  afv2co2  47691