Theorem riotabidv 7377

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868  df-iota 6493  df-riota 7375

This theorem is used by:  riotaeqbidv  7378  csbriota  7390  sup0riota  9451  infval  9472  ttrcltr  9710  fin23lem27  10399  subval  11541  divval  11969  flval  13927  ceilval2  13973  cjval  15262  sqrtval  15397  qnumval  16906  qdenval  16907  lubval  18521  glbval  18534  joinval2  18546  meetval2  18560  grpinvval  19184  pj1fval  19901  pj1val  19902  q1pval  26466  coeval  26535  quotval  26606  divsval  28568  ismidb  29276  lmif  29283  islmib  29285  uspgredg2v  29798  usgredg2v  29801  frgrncvvdeqlem8  30900  frgrncvvdeqlem9  30901  grpoinvval  31118  pjhval  31992  nmopadjlei  32683  cdj3lem2  33030  cvmliftlem15  36042  cvmlift2lem4  36050  cvmlift2  36060  cvmlift3lem2  36064  cvmlift3lem4  36066  cvmlift3lem6  36068  cvmlift3lem7  36069  cvmlift3lem9  36071  cvmlift3  36072  fvtransport  36777  lshpkrlem1  40147  lshpkrlem2  40148  lshpkrlem3  40149  lshpkrcl  40153  trlset  41198  trlval  41199  cdleme27b  41405  cdleme29b  41412  cdleme31so  41416  cdleme31sn1  41418  cdleme31sn1c  41425  cdleme31fv  41427  cdlemefrs29clN  41436  cdleme40v  41506  cdlemg1cN  41624  cdlemg1cex  41625  cdlemksv  41881  cdlemkuu  41932  cdlemkid3N  41970  cdlemkid4  41971  cdlemm10N  42155  dicval  42213  dihval  42269  dochfl1  42513  lcfl7N  42538  lcfrlem8  42586  lcfrlem9  42587  lcf1o  42588  mapdhval  42761  hvmapval  42797  hvmapvalvalN  42798  hdmap1fval  42833  hdmap1vallem  42834  hdmap1val  42835  hdmap1cbv  42839  hdmapfval  42864  hdmapval  42865  hgmapffval  42922  hgmapfval  42923  hgmapval  42924  resubval  43398  redivvald  43473  unxpwdom3  44081  mpaaval  44137