Theorem iotabidv 6494

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1552   = wceq 1554  ℩cio 6464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-v 3450  df-ss 3916  df-uni 4860  df-iota 6466

This theorem is referenced by:  csbiota  6503  dffv3  6852  fveq1  6855  fveq2  6856  fvres  6875  csbfv12  6901  opabiota  6938  fvco2  6953  fvopab5  6998  riotaeqdv  7343  riotabidv  7344  riotabidva  7361  erov  8784  iunfictbso  10060  isf32lem9  10308  shftval  15077  sumeq1  15692  sumeq2w  15695  sumeq2ii  15696  sumeq2sdv  15706  zsum  15721  isumclim3  15762  isumshft  15845  prodeq1f  15912  prodeq1  15913  prodeq2w  15916  prodeq2ii  15917  prodeq2sdv  15929  zprod  15943  iprodclim3  16006  pcval  16856  grpidval  18671  grpidpropd  18672  gsumvalx  18686  gsumpropd  18688  gsumpropd2lem  18689  gsumress  18692  psgnfval  19516  psgnval  19523  psgndif  21627  dchrptlem1  27298  lgsdchrval  27388  nosupcbv  27736  nosupfv  27740  noinfcbv  27751  noinffv  27755  ajval  31003  adjval  32032  urpropd  33365  resv1r  33479  opprqus0g  33632  prodeq12sdv  36526  cbvsumdavw  36587  cbvproddavw  36588  cbvsumdavw2  36603  cbvproddavw2  36604  bj-finsumval0  37725  uncov  38048  dfpre2  38924  dfpre3  38925  dfpre4  38927  afv2eq12d  47757  funressndmafv2rn  47765  afv2res  47781  dfafv23  47795  afv2co2  47799