Theorem iotabidv 6417

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ℩cio 6389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-iota 6391

This theorem is referenced by:  csbiota  6426  dffv3  6770  fveq1  6773  fveq2  6774  fvres  6793  csbfv12  6817  opabiota  6851  fvco2  6865  fvopab5  6907  riotaeqdv  7233  riotabidv  7234  riotabidva  7252  erov  8603  iunfictbso  9870  isf32lem9  10117  shftval  14785  sumeq1  15400  sumeq2w  15404  sumeq2ii  15405  zsum  15430  isumclim3  15471  isumshft  15551  prodeq1f  15618  prodeq2w  15622  prodeq2ii  15623  zprod  15647  iprodclim3  15710  pcval  16545  grpidval  18345  grpidpropd  18346  gsumvalx  18360  gsumpropd  18362  gsumpropd2lem  18363  gsumress  18366  psgnfval  19108  psgnval  19115  psgndif  20807  dchrptlem1  26412  lgsdchrval  26502  ajval  29223  adjval  30252  resv1r  31541  nosupcbv  33905  nosupfv  33909  noinfcbv  33920  noinffv  33924  bj-finsumval0  35456  uncov  35758  afv2eq12d  44707  funressndmafv2rn  44715  afv2res  44731  dfafv23  44745  afv2co2  44749