Theorem iotabidv 6477

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

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

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 3443  df-ss 3919  df-uni 4865  df-iota 6449

This theorem is referenced by:  csbiota  6486  dffv3  6831  fveq1  6834  fveq2  6835  fvres  6854  csbfv12  6880  opabiota  6917  fvco2  6932  fvopab5  6976  riotaeqdv  7318  riotabidv  7319  riotabidva  7336  erov  8755  iunfictbso  10028  isf32lem9  10275  shftval  15001  sumeq1  15616  sumeq2w  15619  sumeq2ii  15620  sumeq2sdv  15630  zsum  15645  isumclim3  15686  isumshft  15766  prodeq1f  15833  prodeq1  15834  prodeq2w  15837  prodeq2ii  15838  prodeq2sdv  15850  zprod  15864  iprodclim3  15927  pcval  16776  grpidval  18590  grpidpropd  18591  gsumvalx  18605  gsumpropd  18607  gsumpropd2lem  18608  gsumress  18611  psgnfval  19433  psgnval  19440  psgndif  21561  dchrptlem1  27235  lgsdchrval  27325  nosupcbv  27674  nosupfv  27678  noinfcbv  27689  noinffv  27693  ajval  30919  adjval  31948  urpropd  33294  resv1r  33401  opprqus0g  33552  prodeq12sdv  36393  cbvsumdavw  36454  cbvproddavw  36455  cbvsumdavw2  36470  cbvproddavw2  36471  bj-finsumval0  37461  uncov  37773  dfpre2  38649  dfpre3  38650  dfpre4  38652  afv2eq12d  47497  funressndmafv2rn  47505  afv2res  47521  dfafv23  47535  afv2co2  47539