Theorem riotabidv 7372

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-iota 6489  df-riota 7370

This theorem is used by:  riotaeqbidv  7373  csbriota  7385  sup0riota  9436  infval  9457  ttrcltr  9695  fin23lem27  10330  subval  11472  divval  11898  flval  13855  ceilval2  13901  cjval  15189  sqrtval  15324  qnumval  16828  qdenval  16829  lubval  18442  glbval  18455  joinval2  18467  meetval2  18481  grpinvval  19104  pj1fval  19821  pj1val  19822  q1pval  26380  coeval  26449  quotval  26522  divsval  28454  ismidb  29162  lmif  29169  islmib  29171  uspgredg2v  29684  usgredg2v  29687  frgrncvvdeqlem8  30786  frgrncvvdeqlem9  30787  grpoinvval  31004  pjhval  31878  nmopadjlei  32569  cdj3lem2  32916  cvmliftlem15  35877  cvmlift2lem4  35885  cvmlift2  35895  cvmlift3lem2  35899  cvmlift3lem4  35901  cvmlift3lem6  35903  cvmlift3lem7  35904  cvmlift3lem9  35906  cvmlift3  35907  fvtransport  36612  lshpkrlem1  39983  lshpkrlem2  39984  lshpkrlem3  39985  lshpkrcl  39989  trlset  41034  trlval  41035  cdleme27b  41241  cdleme29b  41248  cdleme31so  41252  cdleme31sn1  41254  cdleme31sn1c  41261  cdleme31fv  41263  cdlemefrs29clN  41272  cdleme40v  41342  cdlemg1cN  41460  cdlemg1cex  41461  cdlemksv  41717  cdlemkuu  41768  cdlemkid3N  41806  cdlemkid4  41807  cdlemm10N  41991  dicval  42049  dihval  42105  dochfl1  42349  lcfl7N  42374  lcfrlem8  42422  lcfrlem9  42423  lcf1o  42424  mapdhval  42597  hvmapval  42633  hvmapvalvalN  42634  hdmap1fval  42669  hdmap1vallem  42670  hdmap1val  42671  hdmap1cbv  42675  hdmapfval  42700  hdmapval  42701  hgmapffval  42758  hgmapfval  42759  hgmapval  42760  resubval  43242  redivvald  43317  unxpwdom3  43936  mpaaval  43992