Theorem iotabidv 6545

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  ℩cio 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-iota 6514

This theorem is referenced by:  csbiota  6554  dffv3  6902  fveq1  6905  fveq2  6906  fvres  6925  csbfv12  6954  opabiota  6991  fvco2  7006  fvopab5  7049  riotaeqdv  7389  riotabidv  7390  riotabidva  7407  erov  8854  iunfictbso  10154  isf32lem9  10401  shftval  15113  sumeq1  15725  sumeq2w  15728  sumeq2ii  15729  sumeq2sdv  15739  zsum  15754  isumclim3  15795  isumshft  15875  prodeq1f  15942  prodeq1  15943  prodeq2w  15946  prodeq2ii  15947  prodeq2sdv  15959  zprod  15973  iprodclim3  16036  pcval  16882  grpidval  18674  grpidpropd  18675  gsumvalx  18689  gsumpropd  18691  gsumpropd2lem  18692  gsumress  18695  psgnfval  19518  psgnval  19525  psgndif  21620  dchrptlem1  27308  lgsdchrval  27398  nosupcbv  27747  nosupfv  27751  noinfcbv  27762  noinffv  27766  ajval  30880  adjval  31909  urpropd  33236  resv1r  33368  opprqus0g  33518  prodeq12sdv  36219  cbvsumdavw  36280  cbvproddavw  36281  cbvsumdavw2  36296  cbvproddavw2  36297  bj-finsumval0  37286  uncov  37608  afv2eq12d  47227  funressndmafv2rn  47235  afv2res  47251  dfafv23  47265  afv2co2  47269