Theorem riotabidv 7375

Description: Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)

Hypothesis

Ref	Expression
riotabidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
riotabidv	⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem riotabidv

Step	Hyp	Ref	Expression
1		riotabidv.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	anbi2d 642	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	iotabidv 6524	. 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-riota 7373	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-riota 7373	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3eqtr4g 2825	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ℩cio 6494  ℩crio 7372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-uni 4875  df-iota 6496  df-riota 7373

This theorem is used by:  riotaeqbidv  7376  csbriota  7388  sup0riota  9429  infval  9450  ttrcltr  9688  fin23lem27  10323  subval  11459  divval  11885  flval  13840  ceilval2  13886  cjval  15172  sqrtval  15307  qnumval  16813  qdenval  16814  lubval  18427  glbval  18440  joinval2  18452  meetval2  18466  grpinvval  19070  pj1fval  19787  pj1val  19788  q1pval  26341  coeval  26409  quotval  26482  divsval  28411  ismidb  29116  lmif  29123  islmib  29125  uspgredg2v  29603  usgredg2v  29606  frgrncvvdeqlem8  30686  frgrncvvdeqlem9  30687  grpoinvval  30904  pjhval  31778  nmopadjlei  32469  cdj3lem2  32816  cvmliftlem15  35803  cvmlift2lem4  35811  cvmlift2  35821  cvmlift3lem2  35825  cvmlift3lem4  35827  cvmlift3lem6  35829  cvmlift3lem7  35830  cvmlift3lem9  35832  cvmlift3  35833  fvtransport  36537  lshpkrlem1  39917  lshpkrlem2  39918  lshpkrlem3  39919  lshpkrcl  39923  trlset  40968  trlval  40969  cdleme27b  41175  cdleme29b  41182  cdleme31so  41186  cdleme31sn1  41188  cdleme31sn1c  41195  cdleme31fv  41197  cdlemefrs29clN  41206  cdleme40v  41276  cdlemg1cN  41394  cdlemg1cex  41395  cdlemksv  41651  cdlemkuu  41702  cdlemkid3N  41740  cdlemkid4  41741  cdlemm10N  41925  dicval  41983  dihval  42039  dochfl1  42283  lcfl7N  42308  lcfrlem8  42356  lcfrlem9  42357  lcf1o  42358  mapdhval  42531  hvmapval  42567  hvmapvalvalN  42568  hdmap1fval  42603  hdmap1vallem  42604  hdmap1val  42605  hdmap1cbv  42609  hdmapfval  42634  hdmapval  42635  hgmapffval  42692  hgmapfval  42693  hgmapval  42694  resubval  43161  redivvald  43236  unxpwdom3  43855  mpaaval  43911