Theorem riotabidv 7349

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ℩cio 6469  ℩crio 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-uni 4863  df-iota 6471  df-riota 7347

This theorem is referenced by:  riotaeqbidv  7350  csbriota  7362  sup0riota  9405  infval  9426  ttrcltr  9664  fin23lem27  10278  subval  11414  divval  11840  flval  13797  ceilval2  13843  cjval  15119  sqrtval  15254  qnumval  16762  qdenval  16763  lubval  18376  glbval  18389  joinval2  18401  meetval2  18415  grpinvval  19012  pj1fval  19724  pj1val  19725  q1pval  26202  coeval  26270  quotval  26343  divsval  28269  ismidb  28934  lmif  28941  islmib  28943  uspgredg2v  29381  usgredg2v  29384  frgrncvvdeqlem8  30464  frgrncvvdeqlem9  30465  grpoinvval  30682  pjhval  31556  nmopadjlei  32247  cdj3lem2  32594  cvmliftlem15  35608  cvmlift2lem4  35616  cvmlift2  35626  cvmlift3lem2  35630  cvmlift3lem4  35632  cvmlift3lem6  35634  cvmlift3lem7  35635  cvmlift3lem9  35637  cvmlift3  35638  fvtransport  36342  lshpkrlem1  39694  lshpkrlem2  39695  lshpkrlem3  39696  lshpkrcl  39700  trlset  40745  trlval  40746  cdleme27b  40952  cdleme29b  40959  cdleme31so  40963  cdleme31sn1  40965  cdleme31sn1c  40972  cdleme31fv  40974  cdlemefrs29clN  40983  cdleme40v  41053  cdlemg1cN  41171  cdlemg1cex  41172  cdlemksv  41428  cdlemkuu  41479  cdlemkid3N  41517  cdlemkid4  41518  cdlemm10N  41702  dicval  41760  dihval  41816  dochfl1  42060  lcfl7N  42085  lcfrlem8  42133  lcfrlem9  42134  lcf1o  42135  mapdhval  42308  hvmapval  42344  hvmapvalvalN  42345  hdmap1fval  42380  hdmap1vallem  42381  hdmap1val  42382  hdmap1cbv  42386  hdmapfval  42411  hdmapval  42412  hgmapffval  42469  hgmapfval  42470  hgmapval  42471  resubval  42936  redivvald  43011  unxpwdom3  43632  mpaaval  43688