Theorem riotabidv 7382

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099  ℩cio 6504  ℩crio 7379

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 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3964  df-uni 4914  df-iota 6506  df-riota 7380

This theorem is referenced by:  riotaeqbidv  7383  csbriota  7396  sup0riota  9508  infval  9529  ttrcltr  9759  fin23lem27  10371  subval  11501  divval  11925  flval  13814  ceilval2  13860  cjval  15107  sqrtval  15242  qnumval  16739  qdenval  16740  lubval  18381  glbval  18394  joinval2  18406  meetval2  18420  grpinvval  18975  pj1fval  19692  pj1val  19693  q1pval  26182  coeval  26250  quotval  26320  divsval  28190  ismidb  28705  lmif  28712  islmib  28714  uspgredg2v  29160  usgredg2v  29163  frgrncvvdeqlem8  30239  frgrncvvdeqlem9  30240  grpoinvval  30456  pjhval  31330  nmopadjlei  32021  cdj3lem2  32368  cvmliftlem15  35126  cvmlift2lem4  35134  cvmlift2  35144  cvmlift3lem2  35148  cvmlift3lem4  35150  cvmlift3lem6  35152  cvmlift3lem7  35153  cvmlift3lem9  35155  cvmlift3  35156  fvtransport  35856  lshpkrlem1  38808  lshpkrlem2  38809  lshpkrlem3  38810  lshpkrcl  38814  trlset  39860  trlval  39861  cdleme27b  40067  cdleme29b  40074  cdleme31so  40078  cdleme31sn1  40080  cdleme31sn1c  40087  cdleme31fv  40089  cdlemefrs29clN  40098  cdleme40v  40168  cdlemg1cN  40286  cdlemg1cex  40287  cdlemksv  40543  cdlemkuu  40594  cdlemkid3N  40632  cdlemkid4  40633  cdlemm10N  40817  dicval  40875  dihval  40931  dochfl1  41175  lcfl7N  41200  lcfrlem8  41248  lcfrlem9  41249  lcf1o  41250  mapdhval  41423  hvmapval  41459  hvmapvalvalN  41460  hdmap1fval  41495  hdmap1vallem  41496  hdmap1val  41497  hdmap1cbv  41501  hdmapfval  41526  hdmapval  41527  hgmapffval  41584  hgmapfval  41585  hgmapval  41586  resubval  42147  unxpwdom3  42756  mpaaval  42812