Theorem riotabidv 7312

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ℩cio 6440  ℩crio 7309

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-uni 4862  df-iota 6442  df-riota 7310

This theorem is referenced by:  riotaeqbidv  7313  csbriota  7325  sup0riota  9375  infval  9396  ttrcltr  9631  fin23lem27  10241  subval  11372  divval  11799  flval  13716  ceilval2  13762  cjval  15027  sqrtval  15162  qnumval  16666  qdenval  16667  lubval  18278  glbval  18291  joinval2  18303  meetval2  18317  grpinvval  18877  pj1fval  19591  pj1val  19592  q1pval  26076  coeval  26144  quotval  26216  divsval  28115  ismidb  28741  lmif  28748  islmib  28750  uspgredg2v  29187  usgredg2v  29190  frgrncvvdeqlem8  30268  frgrncvvdeqlem9  30269  grpoinvval  30485  pjhval  31359  nmopadjlei  32050  cdj3lem2  32397  cvmliftlem15  35270  cvmlift2lem4  35278  cvmlift2  35288  cvmlift3lem2  35292  cvmlift3lem4  35294  cvmlift3lem6  35296  cvmlift3lem7  35297  cvmlift3lem9  35299  cvmlift3  35300  fvtransport  36005  lshpkrlem1  39088  lshpkrlem2  39089  lshpkrlem3  39090  lshpkrcl  39094  trlset  40140  trlval  40141  cdleme27b  40347  cdleme29b  40354  cdleme31so  40358  cdleme31sn1  40360  cdleme31sn1c  40367  cdleme31fv  40369  cdlemefrs29clN  40378  cdleme40v  40448  cdlemg1cN  40566  cdlemg1cex  40567  cdlemksv  40823  cdlemkuu  40874  cdlemkid3N  40912  cdlemkid4  40913  cdlemm10N  41097  dicval  41155  dihval  41211  dochfl1  41455  lcfl7N  41480  lcfrlem8  41528  lcfrlem9  41529  lcf1o  41530  mapdhval  41703  hvmapval  41739  hvmapvalvalN  41740  hdmap1fval  41775  hdmap1vallem  41776  hdmap1val  41777  hdmap1cbv  41781  hdmapfval  41806  hdmapval  41807  hgmapffval  41864  hgmapfval  41865  hgmapval  41866  resubval  42340  redivvald  42415  unxpwdom3  43068  mpaaval  43124