Theorem iotabidv 6520

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1566   = wceq 1568  ℩cio 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-uni 4872  df-iota 6492

This theorem is referenced by:  csbiota  6529  dffv3  6877  fveq1  6880  fveq2  6881  fvres  6900  csbfv12  6926  opabiota  6963  fvco2  6978  fvopab5  7023  riotaeqdv  7368  riotabidv  7369  riotabidva  7386  erov  8811  iunfictbso  10097  isf32lem9  10344  shftval  15111  sumeq1  15740  sumeq2w  15743  sumeq2ii  15744  sumeq2sdv  15754  zsum  15769  isumclim3  15810  isumshft  15893  prodeq1f  15960  prodeq1  15961  prodeq2w  15964  prodeq2ii  15965  prodeq2sdv  15977  zprod  15991  iprodclim3  16054  pcval  16903  grpidval  18718  grpidpropd  18719  gsumvalx  18733  gsumpropd  18735  gsumpropd2lem  18736  gsumress  18739  psgnfval  19569  psgnval  19576  psgndif  21731  dchrptlem1  27404  lgsdchrval  27494  nosupcbv  27842  nosupfv  27846  noinfcbv  27857  noinffv  27861  ajval  31179  adjval  32208  urpropd  33516  resv1r  33625  opprqus0g  33738  prodeq12sdv  36696  cbvsumdavw  36757  cbvproddavw  36758  cbvsumdavw2  36773  cbvproddavw2  36774  bj-finsumval0  37895  uncov  38218  dfpre2  39094  dfpre3  39095  dfpre4  39097  afv2eq12d  47919  funressndmafv2rn  47927  afv2res  47943  dfafv23  47957  afv2co2  47961