Theorem riotabidv 7119

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ℩cio 6315  ℩crio 7116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946  df-ss 3955  df-uni 4842  df-iota 6317  df-riota 7117

This theorem is referenced by:  riotaeqbidv  7120  csbriota  7132  sup0riota  8932  infval  8953  fin23lem27  9753  subval  10880  divval  11303  flval  13167  ceilval2  13213  cjval  14464  sqrtval  14599  qnumval  16080  qdenval  16081  lubval  17597  glbval  17610  joinval2  17622  meetval2  17636  grpinvval  18147  pj1fval  18823  pj1val  18824  q1pval  24750  coeval  24816  quotval  24884  ismidb  26567  lmif  26574  islmib  26576  uspgredg2v  27009  usgredg2v  27012  frgrncvvdeqlem8  28088  frgrncvvdeqlem9  28089  grpoinvval  28303  pjhval  29177  nmopadjlei  29868  cdj3lem2  30215  cvmliftlem15  32549  cvmlift2lem4  32557  cvmlift2  32567  cvmlift3lem2  32571  cvmlift3lem4  32573  cvmlift3lem6  32575  cvmlift3lem7  32576  cvmlift3lem9  32578  cvmlift3  32579  fvtransport  33497  lshpkrlem1  36250  lshpkrlem2  36251  lshpkrlem3  36252  lshpkrcl  36256  trlset  37301  trlval  37302  cdleme27b  37508  cdleme29b  37515  cdleme31so  37519  cdleme31sn1  37521  cdleme31sn1c  37528  cdleme31fv  37530  cdlemefrs29clN  37539  cdleme40v  37609  cdlemg1cN  37727  cdlemg1cex  37728  cdlemksv  37984  cdlemkuu  38035  cdlemkid3N  38073  cdlemkid4  38074  cdlemm10N  38258  dicval  38316  dihval  38372  dochfl1  38616  lcfl7N  38641  lcfrlem8  38689  lcfrlem9  38690  lcf1o  38691  mapdhval  38864  hvmapval  38900  hvmapvalvalN  38901  hdmap1fval  38936  hdmap1vallem  38937  hdmap1val  38938  hdmap1cbv  38942  hdmapfval  38967  hdmapval  38968  hgmapffval  39025  hgmapfval  39026  hgmapval  39027  resubval  39203  unxpwdom3  39701  mpaaval  39757