Theorem riotabidv 7319

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ℩cio 6443  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842  df-iota 6445  df-riota 7317

This theorem is referenced by:  riotaeqbidv  7320  csbriota  7332  sup0riota  9373  infval  9394  ttrcltr  9632  fin23lem27  10245  subval  11379  divval  11806  flval  13748  ceilval2  13794  cjval  15059  sqrtval  15194  qnumval  16702  qdenval  16703  lubval  18315  glbval  18328  joinval2  18340  meetval2  18354  grpinvval  18951  pj1fval  19664  pj1val  19665  q1pval  26142  coeval  26210  quotval  26280  divsval  28203  ismidb  28868  lmif  28875  islmib  28877  uspgredg2v  29315  usgredg2v  29318  frgrncvvdeqlem8  30398  frgrncvvdeqlem9  30399  grpoinvval  30616  pjhval  31490  nmopadjlei  32181  cdj3lem2  32528  cvmliftlem15  35541  cvmlift2lem4  35549  cvmlift2  35559  cvmlift3lem2  35563  cvmlift3lem4  35565  cvmlift3lem6  35567  cvmlift3lem7  35568  cvmlift3lem9  35570  cvmlift3  35571  fvtransport  36275  lshpkrlem1  39617  lshpkrlem2  39618  lshpkrlem3  39619  lshpkrcl  39623  trlset  40668  trlval  40669  cdleme27b  40875  cdleme29b  40882  cdleme31so  40886  cdleme31sn1  40888  cdleme31sn1c  40895  cdleme31fv  40897  cdlemefrs29clN  40906  cdleme40v  40976  cdlemg1cN  41094  cdlemg1cex  41095  cdlemksv  41351  cdlemkuu  41402  cdlemkid3N  41440  cdlemkid4  41441  cdlemm10N  41625  dicval  41683  dihval  41739  dochfl1  41983  lcfl7N  42008  lcfrlem8  42056  lcfrlem9  42057  lcf1o  42058  mapdhval  42231  hvmapval  42267  hvmapvalvalN  42268  hdmap1fval  42303  hdmap1vallem  42304  hdmap1val  42305  hdmap1cbv  42309  hdmapfval  42334  hdmapval  42335  hgmapffval  42392  hgmapfval  42393  hgmapval  42394  resubval  42859  redivvald  42934  unxpwdom3  43555  mpaaval  43611