Theorem riotabidv 7305

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ℩cio 6435  ℩crio 7302

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-uni 4860  df-iota 6437  df-riota 7303

This theorem is referenced by:  riotaeqbidv  7306  csbriota  7318  sup0riota  9350  infval  9371  ttrcltr  9606  fin23lem27  10216  subval  11348  divval  11775  flval  13695  ceilval2  13741  cjval  15006  sqrtval  15141  qnumval  16645  qdenval  16646  lubval  18257  glbval  18270  joinval2  18282  meetval2  18296  grpinvval  18890  pj1fval  19604  pj1val  19605  q1pval  26085  coeval  26153  quotval  26225  divsval  28126  ismidb  28754  lmif  28761  islmib  28763  uspgredg2v  29200  usgredg2v  29203  frgrncvvdeqlem8  30281  frgrncvvdeqlem9  30282  grpoinvval  30498  pjhval  31372  nmopadjlei  32063  cdj3lem2  32410  cvmliftlem15  35330  cvmlift2lem4  35338  cvmlift2  35348  cvmlift3lem2  35352  cvmlift3lem4  35354  cvmlift3lem6  35356  cvmlift3lem7  35357  cvmlift3lem9  35359  cvmlift3  35360  fvtransport  36065  lshpkrlem1  39148  lshpkrlem2  39149  lshpkrlem3  39150  lshpkrcl  39154  trlset  40199  trlval  40200  cdleme27b  40406  cdleme29b  40413  cdleme31so  40417  cdleme31sn1  40419  cdleme31sn1c  40426  cdleme31fv  40428  cdlemefrs29clN  40437  cdleme40v  40507  cdlemg1cN  40625  cdlemg1cex  40626  cdlemksv  40882  cdlemkuu  40933  cdlemkid3N  40971  cdlemkid4  40972  cdlemm10N  41156  dicval  41214  dihval  41270  dochfl1  41514  lcfl7N  41539  lcfrlem8  41587  lcfrlem9  41588  lcf1o  41589  mapdhval  41762  hvmapval  41798  hvmapvalvalN  41799  hdmap1fval  41834  hdmap1vallem  41835  hdmap1val  41836  hdmap1cbv  41840  hdmapfval  41865  hdmapval  41866  hgmapffval  41923  hgmapfval  41924  hgmapval  41925  resubval  42399  redivvald  42474  unxpwdom3  43127  mpaaval  43183