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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569  ℩cio 6490

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872  df-iota 6492

This theorem is used by:  csbiota  6529  dffv3  6877  fveq1  6880  fveq2  6881  fvres  6900  csbfv12  6926  opabiota  6963  fvco2  6978  fvopab5  7023  riotaeqdv  7370  riotabidv  7371  riotabidva  7388  erov  8810  iunfictbso  10105  isf32lem9  10351  shftval  15118  sumeq1  15747  sumeq2w  15750  sumeq2ii  15751  sumeq2sdv  15761  zsum  15776  isumclim3  15817  isumshft  15900  prodeq1f  15967  prodeq1  15968  prodeq2w  15971  prodeq2ii  15972  prodeq2sdv  15984  zprod  15998  iprodclim3  16061  pcval  16910  grpidval  18725  grpidpropd  18726  gsumvalx  18740  gsumpropd  18742  gsumpropd2lem  18743  gsumress  18746  psgnfval  19576  psgnval  19583  psgndif  21763  dchrptlem1  27439  lgsdchrval  27529  nosupcbv  27877  nosupfv  27881  noinfcbv  27892  noinffv  27896  ajval  31224  adjval  32253  urpropd  33559  resv1r  33668  opprqus0g  33781  prodeq12sdv  36758  cbvsumdavw  36819  cbvproddavw  36820  cbvsumdavw2  36835  cbvproddavw2  36836  bj-finsumval0  37957  uncov  38280  dfpre2  39154  dfpre3  39155  dfpre4  39157  afv2eq12d  47980  funressndmafv2rn  47988  afv2res  48004  dfafv23  48018  afv2co2  48022