Theorem iotabidv 6342

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1534   = wceq 1536  ℩cio 6315

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946  df-ss 3955  df-uni 4842  df-iota 6317

This theorem is referenced by:  csbiota  6351  dffv3  6669  fveq1  6672  fveq2  6673  fvres  6692  csbfv12  6716  opabiota  6749  fvco2  6761  fvopab5  6803  riotaeqdv  7118  riotabidv  7119  riotabidva  7136  erov  8397  iunfictbso  9543  isf32lem9  9786  shftval  14436  sumeq1  15048  sumeq2w  15052  sumeq2ii  15053  zsum  15078  isumclim3  15117  isumshft  15197  prodeq1f  15265  prodeq2w  15269  prodeq2ii  15270  zprod  15294  iprodclim3  15357  pcval  16184  grpidval  17874  grpidpropd  17875  gsumvalx  17889  gsumpropd  17891  gsumpropd2lem  17892  gsumress  17895  psgnfval  18631  psgnval  18638  psgndif  20749  dchrptlem1  25843  lgsdchrval  25933  ajval  28641  adjval  29670  resv1r  30914  nosupfv  33210  noeta  33226  bj-finsumval0  34571  uncov  34877  afv2eq12d  43421  funressndmafv2rn  43429  afv2res  43445  dfafv23  43459  afv2co2  43463