Theorem iotabidv 6515

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-iota 6484

This theorem is referenced by:  csbiota  6524  dffv3  6872  fveq1  6875  fveq2  6876  fvres  6895  csbfv12  6924  opabiota  6961  fvco2  6976  fvopab5  7019  riotaeqdv  7363  riotabidv  7364  riotabidva  7381  erov  8828  iunfictbso  10128  isf32lem9  10375  shftval  15093  sumeq1  15705  sumeq2w  15708  sumeq2ii  15709  sumeq2sdv  15719  zsum  15734  isumclim3  15775  isumshft  15855  prodeq1f  15922  prodeq1  15923  prodeq2w  15926  prodeq2ii  15927  prodeq2sdv  15939  zprod  15953  iprodclim3  16016  pcval  16864  grpidval  18639  grpidpropd  18640  gsumvalx  18654  gsumpropd  18656  gsumpropd2lem  18657  gsumress  18660  psgnfval  19481  psgnval  19488  psgndif  21562  dchrptlem1  27227  lgsdchrval  27317  nosupcbv  27666  nosupfv  27670  noinfcbv  27681  noinffv  27685  ajval  30842  adjval  31871  urpropd  33227  resv1r  33355  opprqus0g  33505  prodeq12sdv  36236  cbvsumdavw  36297  cbvproddavw  36298  cbvsumdavw2  36313  cbvproddavw2  36314  bj-finsumval0  37303  uncov  37625  afv2eq12d  47244  funressndmafv2rn  47252  afv2res  47268  dfafv23  47282  afv2co2  47286