Theorem riotabidv 7327

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866  df-iota 6456  df-riota 7325

This theorem is referenced by:  riotaeqbidv  7328  csbriota  7340  sup0riota  9381  infval  9402  ttrcltr  9637  fin23lem27  10250  subval  11383  divval  11810  flval  13726  ceilval2  13772  cjval  15037  sqrtval  15172  qnumval  16676  qdenval  16677  lubval  18289  glbval  18302  joinval2  18314  meetval2  18328  grpinvval  18922  pj1fval  19635  pj1val  19636  q1pval  26128  coeval  26196  quotval  26268  divsval  28197  ismidb  28862  lmif  28869  islmib  28871  uspgredg2v  29309  usgredg2v  29312  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  grpoinvval  30610  pjhval  31484  nmopadjlei  32175  cdj3lem2  32522  cvmliftlem15  35511  cvmlift2lem4  35519  cvmlift2  35529  cvmlift3lem2  35533  cvmlift3lem4  35535  cvmlift3lem6  35537  cvmlift3lem7  35538  cvmlift3lem9  35540  cvmlift3  35541  fvtransport  36245  lshpkrlem1  39483  lshpkrlem2  39484  lshpkrlem3  39485  lshpkrcl  39489  trlset  40534  trlval  40535  cdleme27b  40741  cdleme29b  40748  cdleme31so  40752  cdleme31sn1  40754  cdleme31sn1c  40761  cdleme31fv  40763  cdlemefrs29clN  40772  cdleme40v  40842  cdlemg1cN  40960  cdlemg1cex  40961  cdlemksv  41217  cdlemkuu  41268  cdlemkid3N  41306  cdlemkid4  41307  cdlemm10N  41491  dicval  41549  dihval  41605  dochfl1  41849  lcfl7N  41874  lcfrlem8  41922  lcfrlem9  41923  lcf1o  41924  mapdhval  42097  hvmapval  42133  hvmapvalvalN  42134  hdmap1fval  42169  hdmap1vallem  42170  hdmap1val  42171  hdmap1cbv  42175  hdmapfval  42200  hdmapval  42201  hgmapffval  42258  hgmapfval  42259  hgmapval  42260  resubval  42734  redivvald  42809  unxpwdom3  43449  mpaaval  43505