Theorem iotabidv 6542

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532   = wceq 1534  ℩cio 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-ss 3976  df-uni 4919  df-iota 6510

This theorem is referenced by:  csbiota  6551  dffv3  6901  fveq1  6904  fveq2  6905  fvres  6924  csbfv12  6953  opabiota  6989  fvco2  7004  fvopab5  7047  riotaeqdv  7387  riotabidv  7388  riotabidva  7406  erov  8851  iunfictbso  10164  isf32lem9  10411  shftval  15100  sumeq1  15714  sumeq2w  15717  sumeq2ii  15718  zsum  15743  isumclim3  15784  isumshft  15864  prodeq1f  15931  prodeq2w  15935  prodeq2ii  15936  zprod  15960  iprodclim3  16023  pcval  16867  grpidval  18675  grpidpropd  18676  gsumvalx  18690  gsumpropd  18692  gsumpropd2lem  18693  gsumress  18696  psgnfval  19520  psgnval  19527  psgndif  21620  dchrptlem1  27316  lgsdchrval  27406  nosupcbv  27755  nosupfv  27759  noinfcbv  27770  noinffv  27774  ajval  30817  adjval  31846  urpropd  33126  resv1r  33246  opprqus0g  33396  bj-finsumval0  37039  uncov  37349  afv2eq12d  46898  funressndmafv2rn  46906  afv2res  46922  dfafv23  46936  afv2co2  46940