Theorem iotabidv 6541

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  ℩cio 6510

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-iota 6512

This theorem is used by:  csbiota  6551  dffv3  6904  fveq1  6907  fveq2  6908  fvres  6927  csbfv12  6953  opabiota  6990  fvco2  7005  fvopab5  7050  riotaeqdv  7401  riotabidv  7402  riotabidva  7419  erov  8863  uncov  8921  iunfictbso  10220  isf32lem9  10466  shftval  15256  sumeq1  15885  sumeq2w  15888  sumeq2ii  15889  sumeq2sdv  15899  zsum  15913  isumclim3  15954  isumshft  16037  prodeq1f  16104  prodeq1  16105  prodeq2w  16108  prodeq2ii  16109  prodeq2sdv  16120  zprod  16133  iprodclim3  16196  pcval  17051  grpidval  18869  grpidpropd  18871  gsumvalx  18894  gsumpropd  18896  gsumpropd2lem  18897  gsumress  18900  psgnfval  19744  psgnval  19751  psgndif  21938  dchrptlem1  27621  lgsdchrval  27711  nosupcbv  28089  nosupfv  28093  noinfcbv  28104  noinffv  28108  ajval  31493  adjval  32522  urpropd  33861  resv1r  33970  opprqus0g  34084  prodeq12sdv  37185  cbvsumdavw  37246  cbvproddavw  37247  cbvsumdavw2  37262  cbvproddavw2  37263  bj-finsumval0  38398  dfpre2  39601  dfpre3  39602  dfpre4  39604  afv2eq12d  48490  funressndmafv2rn  48498  afv2res  48514  dfafv23  48528  afv2co2  48532