Theorem riotabidv 7326

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ℩cio 6452  ℩crio 7323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-iota 6454  df-riota 7324

This theorem is referenced by:  riotaeqbidv  7327  csbriota  7339  sup0riota  9379  infval  9400  ttrcltr  9637  fin23lem27  10250  subval  11384  divval  11811  flval  13753  ceilval2  13799  cjval  15064  sqrtval  15199  qnumval  16707  qdenval  16708  lubval  18320  glbval  18333  joinval2  18345  meetval2  18359  grpinvval  18956  pj1fval  19669  pj1val  19670  q1pval  26120  coeval  26188  quotval  26258  divsval  28181  ismidb  28846  lmif  28853  islmib  28855  uspgredg2v  29293  usgredg2v  29296  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  grpoinvval  30594  pjhval  31468  nmopadjlei  32159  cdj3lem2  32506  cvmliftlem15  35480  cvmlift2lem4  35488  cvmlift2  35498  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  cvmlift3  35510  fvtransport  36214  lshpkrlem1  39556  lshpkrlem2  39557  lshpkrlem3  39558  lshpkrcl  39562  trlset  40607  trlval  40608  cdleme27b  40814  cdleme29b  40821  cdleme31so  40825  cdleme31sn1  40827  cdleme31sn1c  40834  cdleme31fv  40836  cdlemefrs29clN  40845  cdleme40v  40915  cdlemg1cN  41033  cdlemg1cex  41034  cdlemksv  41290  cdlemkuu  41341  cdlemkid3N  41379  cdlemkid4  41380  cdlemm10N  41564  dicval  41622  dihval  41678  dochfl1  41922  lcfl7N  41947  lcfrlem8  41995  lcfrlem9  41996  lcf1o  41997  mapdhval  42170  hvmapval  42206  hvmapvalvalN  42207  hdmap1fval  42242  hdmap1vallem  42243  hdmap1val  42244  hdmap1cbv  42248  hdmapfval  42273  hdmapval  42274  hgmapffval  42331  hgmapfval  42332  hgmapval  42333  resubval  42799  redivvald  42874  unxpwdom3  43523  mpaaval  43579