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  7319  riotabidv  7320  riotabidva  7337  erov  8756  iunfictbso  10029  isf32lem9  10276  shftval  15002  sumeq1  15617  sumeq2w  15620  sumeq2ii  15621  sumeq2sdv  15631  zsum  15646  isumclim3  15687  isumshft  15767  prodeq1f  15834  prodeq1  15835  prodeq2w  15838  prodeq2ii  15839  prodeq2sdv  15851  zprod  15865  iprodclim3  15928  pcval  16777  grpidval  18591  grpidpropd  18592  gsumvalx  18606  gsumpropd  18608  gsumpropd2lem  18609  gsumress  18612  psgnfval  19434  psgnval  19441  psgndif  21562  dchrptlem1  27236  lgsdchrval  27326  nosupcbv  27675  nosupfv  27679  noinfcbv  27690  noinffv  27694  ajval  30941  adjval  31970  urpropd  33317  resv1r  33424  opprqus0g  33575  prodeq12sdv  36425  cbvsumdavw  36486  cbvproddavw  36487  cbvsumdavw2  36502  cbvproddavw2  36503  bj-finsumval0  37503  uncov  37815  dfpre2  38691  dfpre3  38692  dfpre4  38694  afv2eq12d  47538  funressndmafv2rn  47546  afv2res  47562  dfafv23  47576  afv2co2  47580