Theorem riotabidv 7118

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ℩cio 6314  ℩crio 7115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841  df-iota 6316  df-riota 7116

This theorem is referenced by:  riotaeqbidv  7119  csbriota  7131  sup0riota  8931  infval  8952  fin23lem27  9752  subval  10879  divval  11302  flval  13167  ceilval2  13213  cjval  14463  sqrtval  14598  qnumval  16079  qdenval  16080  lubval  17596  glbval  17609  joinval2  17621  meetval2  17635  grpinvval  18146  pj1fval  18822  pj1val  18823  q1pval  24749  coeval  24815  quotval  24883  ismidb  26566  lmif  26573  islmib  26575  uspgredg2v  27008  usgredg2v  27011  frgrncvvdeqlem8  28087  frgrncvvdeqlem9  28088  grpoinvval  28302  pjhval  29176  nmopadjlei  29867  cdj3lem2  30214  cvmliftlem15  32547  cvmlift2lem4  32555  cvmlift2  32565  cvmlift3lem2  32569  cvmlift3lem4  32571  cvmlift3lem6  32573  cvmlift3lem7  32574  cvmlift3lem9  32576  cvmlift3  32577  fvtransport  33495  lshpkrlem1  36248  lshpkrlem2  36249  lshpkrlem3  36250  lshpkrcl  36254  trlset  37299  trlval  37300  cdleme27b  37506  cdleme29b  37513  cdleme31so  37517  cdleme31sn1  37519  cdleme31sn1c  37526  cdleme31fv  37528  cdlemefrs29clN  37537  cdleme40v  37607  cdlemg1cN  37725  cdlemg1cex  37726  cdlemksv  37982  cdlemkuu  38033  cdlemkid3N  38071  cdlemkid4  38072  cdlemm10N  38256  dicval  38314  dihval  38370  dochfl1  38614  lcfl7N  38639  lcfrlem8  38687  lcfrlem9  38688  lcf1o  38689  mapdhval  38862  hvmapval  38898  hvmapvalvalN  38899  hdmap1fval  38934  hdmap1vallem  38935  hdmap1val  38936  hdmap1cbv  38940  hdmapfval  38965  hdmapval  38966  hgmapffval  39023  hgmapfval  39024  hgmapval  39025  resubval  39204  unxpwdom3  39702  mpaaval  39758