Theorem iotabidv 6526

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

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

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 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961  df-uni 4904  df-iota 6494

This theorem is referenced by:  csbiota  6535  dffv3  6887  fveq1  6890  fveq2  6891  fvres  6910  csbfv12  6939  opabiota  6975  fvco2  6989  fvopab5  7032  riotaeqdv  7371  riotabidv  7372  riotabidva  7390  erov  8824  iunfictbso  10129  isf32lem9  10376  shftval  15045  sumeq1  15659  sumeq2w  15662  sumeq2ii  15663  zsum  15688  isumclim3  15729  isumshft  15809  prodeq1f  15876  prodeq2w  15880  prodeq2ii  15881  zprod  15905  iprodclim3  15968  pcval  16804  grpidval  18612  grpidpropd  18613  gsumvalx  18627  gsumpropd  18629  gsumpropd2lem  18630  gsumress  18633  psgnfval  19446  psgnval  19453  psgndif  21521  dchrptlem1  27184  lgsdchrval  27274  nosupcbv  27622  nosupfv  27626  noinfcbv  27637  noinffv  27641  ajval  30658  adjval  31687  urpropd  32916  resv1r  32993  opprqus0g  33137  bj-finsumval0  36700  uncov  37009  afv2eq12d  46518  funressndmafv2rn  46526  afv2res  46542  dfafv23  46556  afv2co2  46560