Theorem iotabidv 5910

Description: Formula-building deduction rule 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 1895	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		iotabi 5898	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521   = wceq 1523  ℩cio 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-uni 4469  df-iota 5889

This theorem is referenced by:  csbiota  5919  dffv3  6225  fveq1  6228  fveq2  6229  fvres  6245  csbfv12  6269  opabiota  6300  fvco2  6312  fvopab5  6349  riotaeqdv  6652  riotabidv  6653  riotabidva  6667  erov  7887  iunfictbso  8975  isf32lem9  9221  shftval  13858  sumeq1  14463  sumeq2w  14466  sumeq2ii  14467  zsum  14493  isumclim3  14534  isumshft  14615  prodeq1f  14682  prodeq2w  14686  prodeq2ii  14687  zprod  14711  iprodclim3  14775  pcval  15596  grpidval  17307  grpidpropd  17308  gsumvalx  17317  gsumpropd  17319  gsumpropd2lem  17320  gsumress  17323  psgnfval  17966  psgnval  17973  psgndif  19996  dchrptlem1  25034  lgsdchrval  25124  ajval  27845  adjval  28877  resv1r  29965  nosupfv  31977  noeta  31993  bj-finsumval0  33277  uncov  33520