Theorem riotabidv 7295

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ℩cio 6429  ℩crio 7292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915  df-uni 4853  df-iota 6431  df-riota 7293

This theorem is referenced by:  riotaeqbidv  7296  csbriota  7309  sup0riota  9322  infval  9343  ttrcltr  9573  fin23lem27  10185  subval  11313  divval  11736  flval  13615  ceilval2  13661  cjval  14912  sqrtval  15047  qnumval  16538  qdenval  16539  lubval  18171  glbval  18184  joinval2  18196  meetval2  18210  grpinvval  18716  pj1fval  19395  pj1val  19396  q1pval  25424  coeval  25490  quotval  25558  ismidb  27428  lmif  27435  islmib  27437  uspgredg2v  27880  usgredg2v  27883  frgrncvvdeqlem8  28958  frgrncvvdeqlem9  28959  grpoinvval  29173  pjhval  30047  nmopadjlei  30738  cdj3lem2  31085  cvmliftlem15  33559  cvmlift2lem4  33567  cvmlift2  33577  cvmlift3lem2  33581  cvmlift3lem4  33583  cvmlift3lem6  33585  cvmlift3lem7  33586  cvmlift3lem9  33588  cvmlift3  33589  fvtransport  34430  lshpkrlem1  37377  lshpkrlem2  37378  lshpkrlem3  37379  lshpkrcl  37383  trlset  38429  trlval  38430  cdleme27b  38636  cdleme29b  38643  cdleme31so  38647  cdleme31sn1  38649  cdleme31sn1c  38656  cdleme31fv  38658  cdlemefrs29clN  38667  cdleme40v  38737  cdlemg1cN  38855  cdlemg1cex  38856  cdlemksv  39112  cdlemkuu  39163  cdlemkid3N  39201  cdlemkid4  39202  cdlemm10N  39386  dicval  39444  dihval  39500  dochfl1  39744  lcfl7N  39769  lcfrlem8  39817  lcfrlem9  39818  lcf1o  39819  mapdhval  39992  hvmapval  40028  hvmapvalvalN  40029  hdmap1fval  40064  hdmap1vallem  40065  hdmap1val  40066  hdmap1cbv  40070  hdmapfval  40095  hdmapval  40096  hgmapffval  40153  hgmapfval  40154  hgmapval  40155  resubval  40610  unxpwdom3  41183  mpaaval  41239