Theorem riotabidv 7406

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ℩cio 6523  ℩crio 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-iota 6525  df-riota 7404

This theorem is referenced by:  riotaeqbidv  7407  csbriota  7420  sup0riota  9534  infval  9555  ttrcltr  9785  fin23lem27  10397  subval  11527  divval  11951  flval  13845  ceilval2  13891  cjval  15151  sqrtval  15286  qnumval  16784  qdenval  16785  lubval  18426  glbval  18439  joinval2  18451  meetval2  18465  grpinvval  19020  pj1fval  19736  pj1val  19737  q1pval  26214  coeval  26282  quotval  26352  divsval  28233  ismidb  28804  lmif  28811  islmib  28813  uspgredg2v  29259  usgredg2v  29262  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  grpoinvval  30555  pjhval  31429  nmopadjlei  32120  cdj3lem2  32467  cvmliftlem15  35266  cvmlift2lem4  35274  cvmlift2  35284  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  fvtransport  35996  lshpkrlem1  39066  lshpkrlem2  39067  lshpkrlem3  39068  lshpkrcl  39072  trlset  40118  trlval  40119  cdleme27b  40325  cdleme29b  40332  cdleme31so  40336  cdleme31sn1  40338  cdleme31sn1c  40345  cdleme31fv  40347  cdlemefrs29clN  40356  cdleme40v  40426  cdlemg1cN  40544  cdlemg1cex  40545  cdlemksv  40801  cdlemkuu  40852  cdlemkid3N  40890  cdlemkid4  40891  cdlemm10N  41075  dicval  41133  dihval  41189  dochfl1  41433  lcfl7N  41458  lcfrlem8  41506  lcfrlem9  41507  lcf1o  41508  mapdhval  41681  hvmapval  41717  hvmapvalvalN  41718  hdmap1fval  41753  hdmap1vallem  41754  hdmap1val  41755  hdmap1cbv  41759  hdmapfval  41784  hdmapval  41785  hgmapffval  41842  hgmapfval  41843  hgmapval  41844  resubval  42343  unxpwdom3  43052  mpaaval  43108