Theorem riotabidv 7359

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 641	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	iotabidv 6509	. 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-riota 7357	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-riota 7357	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3eqtr4g 2825	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ℩cio 6479  ℩crio 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-uni 4868  df-iota 6481  df-riota 7357

This theorem is referenced by:  riotaeqbidv  7360  csbriota  7372  sup0riota  9414  infval  9435  ttrcltr  9673  fin23lem27  10300  subval  11436  divval  11862  flval  13815  ceilval2  13861  cjval  15141  sqrtval  15276  qnumval  16784  qdenval  16785  lubval  18398  glbval  18411  joinval2  18423  meetval2  18437  grpinvval  19035  pj1fval  19752  pj1val  19753  q1pval  26269  coeval  26337  quotval  26410  divsval  28336  ismidb  29026  lmif  29033  islmib  29035  uspgredg2v  29479  usgredg2v  29482  frgrncvvdeqlem8  30562  frgrncvvdeqlem9  30563  grpoinvval  30780  pjhval  31654  nmopadjlei  32345  cdj3lem2  32692  cvmliftlem15  35656  cvmlift2lem4  35664  cvmlift2  35674  cvmlift3lem2  35678  cvmlift3lem4  35680  cvmlift3lem6  35682  cvmlift3lem7  35683  cvmlift3lem9  35685  cvmlift3  35686  fvtransport  36390  lshpkrlem1  39741  lshpkrlem2  39742  lshpkrlem3  39743  lshpkrcl  39747  trlset  40792  trlval  40793  cdleme27b  40999  cdleme29b  41006  cdleme31so  41010  cdleme31sn1  41012  cdleme31sn1c  41019  cdleme31fv  41021  cdlemefrs29clN  41030  cdleme40v  41100  cdlemg1cN  41218  cdlemg1cex  41219  cdlemksv  41475  cdlemkuu  41526  cdlemkid3N  41564  cdlemkid4  41565  cdlemm10N  41749  dicval  41807  dihval  41863  dochfl1  42107  lcfl7N  42132  lcfrlem8  42180  lcfrlem9  42181  lcf1o  42182  mapdhval  42355  hvmapval  42391  hvmapvalvalN  42392  hdmap1fval  42427  hdmap1vallem  42428  hdmap1val  42429  hdmap1cbv  42433  hdmapfval  42458  hdmapval  42459  hgmapffval  42516  hgmapfval  42517  hgmapval  42518  resubval  42983  redivvald  43058  unxpwdom3  43679  mpaaval  43735