Theorem iotabidv 6547

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537  ℩cio 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-iota 6516

This theorem is referenced by:  csbiota  6556  dffv3  6903  fveq1  6906  fveq2  6907  fvres  6926  csbfv12  6955  opabiota  6991  fvco2  7006  fvopab5  7049  riotaeqdv  7389  riotabidv  7390  riotabidva  7407  erov  8853  iunfictbso  10152  isf32lem9  10399  shftval  15110  sumeq1  15722  sumeq2w  15725  sumeq2ii  15726  sumeq2sdv  15736  zsum  15751  isumclim3  15792  isumshft  15872  prodeq1f  15939  prodeq1  15940  prodeq2w  15943  prodeq2ii  15944  prodeq2sdv  15956  zprod  15970  iprodclim3  16033  pcval  16878  grpidval  18687  grpidpropd  18688  gsumvalx  18702  gsumpropd  18704  gsumpropd2lem  18705  gsumress  18708  psgnfval  19533  psgnval  19540  psgndif  21638  dchrptlem1  27323  lgsdchrval  27413  nosupcbv  27762  nosupfv  27766  noinfcbv  27777  noinffv  27781  ajval  30890  adjval  31919  urpropd  33222  resv1r  33348  opprqus0g  33498  prodeq12sdv  36201  cbvsumdavw  36262  cbvproddavw  36263  cbvsumdavw2  36278  cbvproddavw2  36279  bj-finsumval0  37268  uncov  37588  afv2eq12d  47165  funressndmafv2rn  47173  afv2res  47189  dfafv23  47203  afv2co2  47207