Theorem iotabidv 6461

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541  ℩cio 6431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-ss 3917  df-uni 4858  df-iota 6433

This theorem is referenced by:  csbiota  6470  dffv3  6813  fveq1  6816  fveq2  6817  fvres  6836  csbfv12  6862  opabiota  6899  fvco2  6914  fvopab5  6957  riotaeqdv  7299  riotabidv  7300  riotabidva  7317  erov  8733  iunfictbso  9997  isf32lem9  10244  shftval  14973  sumeq1  15588  sumeq2w  15591  sumeq2ii  15592  sumeq2sdv  15602  zsum  15617  isumclim3  15658  isumshft  15738  prodeq1f  15805  prodeq1  15806  prodeq2w  15809  prodeq2ii  15810  prodeq2sdv  15822  zprod  15836  iprodclim3  15899  pcval  16748  grpidval  18561  grpidpropd  18562  gsumvalx  18576  gsumpropd  18578  gsumpropd2lem  18579  gsumress  18582  psgnfval  19405  psgnval  19412  psgndif  21532  dchrptlem1  27195  lgsdchrval  27285  nosupcbv  27634  nosupfv  27638  noinfcbv  27649  noinffv  27653  ajval  30831  adjval  31860  urpropd  33189  resv1r  33294  opprqus0g  33445  prodeq12sdv  36231  cbvsumdavw  36292  cbvproddavw  36293  cbvsumdavw2  36308  cbvproddavw2  36309  bj-finsumval0  37298  uncov  37620  afv2eq12d  47225  funressndmafv2rn  47233  afv2res  47249  dfafv23  47263  afv2co2  47267