Theorem riotabidv 7390

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ℩cio 6514  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-iota 6516  df-riota 7388

This theorem is referenced by:  riotaeqbidv  7391  csbriota  7403  sup0riota  9503  infval  9524  ttrcltr  9754  fin23lem27  10366  subval  11497  divval  11922  flval  13831  ceilval2  13877  cjval  15138  sqrtval  15273  qnumval  16771  qdenval  16772  lubval  18414  glbval  18427  joinval2  18439  meetval2  18453  grpinvval  19011  pj1fval  19727  pj1val  19728  q1pval  26209  coeval  26277  quotval  26349  divsval  28230  ismidb  28801  lmif  28808  islmib  28810  uspgredg2v  29256  usgredg2v  29259  frgrncvvdeqlem8  30335  frgrncvvdeqlem9  30336  grpoinvval  30552  pjhval  31426  nmopadjlei  32117  cdj3lem2  32464  cvmliftlem15  35283  cvmlift2lem4  35291  cvmlift2  35301  cvmlift3lem2  35305  cvmlift3lem4  35307  cvmlift3lem6  35309  cvmlift3lem7  35310  cvmlift3lem9  35312  cvmlift3  35313  fvtransport  36014  lshpkrlem1  39092  lshpkrlem2  39093  lshpkrlem3  39094  lshpkrcl  39098  trlset  40144  trlval  40145  cdleme27b  40351  cdleme29b  40358  cdleme31so  40362  cdleme31sn1  40364  cdleme31sn1c  40371  cdleme31fv  40373  cdlemefrs29clN  40382  cdleme40v  40452  cdlemg1cN  40570  cdlemg1cex  40571  cdlemksv  40827  cdlemkuu  40878  cdlemkid3N  40916  cdlemkid4  40917  cdlemm10N  41101  dicval  41159  dihval  41215  dochfl1  41459  lcfl7N  41484  lcfrlem8  41532  lcfrlem9  41533  lcf1o  41534  mapdhval  41707  hvmapval  41743  hvmapvalvalN  41744  hdmap1fval  41779  hdmap1vallem  41780  hdmap1val  41781  hdmap1cbv  41785  hdmapfval  41810  hdmapval  41811  hgmapffval  41868  hgmapfval  41869  hgmapval  41870  resubval  42374  unxpwdom3  43084  mpaaval  43140