Theorem riotabidv 7410

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ℩cio 6518  ℩crio 7407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4873  df-iota 6520  df-riota 7408

This theorem is used by:  riotaeqbidv  7411  csbriota  7423  sup0riota  9495  infval  9516  ttrcltr  9754  fin23lem27  10445  subval  11587  divval  12016  flval  13974  ceilval2  14020  cjval  15312  sqrtval  15447  qnumval  16957  qdenval  16958  lubval  18578  glbval  18591  joinval2  18603  meetval2  18617  grpinvval  19241  pj1fval  19959  pj1val  19960  q1pval  26528  coeval  26597  quotval  26668  divsval  28632  ismidb  29340  lmif  29347  islmib  29349  uspgredg2v  29862  usgredg2v  29865  frgrncvvdeqlem8  30964  frgrncvvdeqlem9  30965  grpoinvval  31182  pjhval  32056  nmopadjlei  32747  cdj3lem2  33094  cvmliftlem15  36271  cvmlift2lem4  36279  cvmlift2  36289  cvmlift3lem2  36293  cvmlift3lem4  36295  cvmlift3lem6  36297  cvmlift3lem7  36298  cvmlift3lem9  36300  cvmlift3  36301  fvtransport  37012  lshpkrlem1  40433  lshpkrlem2  40434  lshpkrlem3  40435  lshpkrcl  40439  trlset  41484  trlval  41485  cdleme27b  41691  cdleme29b  41698  cdleme31so  41702  cdleme31sn1  41704  cdleme31sn1c  41711  cdleme31fv  41713  cdlemefrs29clN  41722  cdleme40v  41792  cdlemg1cN  41910  cdlemg1cex  41911  cdlemksv  42167  cdlemkuu  42218  cdlemkid3N  42256  cdlemkid4  42257  cdlemm10N  42441  dicval  42499  dihval  42555  dochfl1  42799  lcfl7N  42824  lcfrlem8  42872  lcfrlem9  42873  lcf1o  42874  mapdhval  43047  hvmapval  43083  hvmapvalvalN  43084  hdmap1fval  43119  hdmap1vallem  43120  hdmap1val  43121  hdmap1cbv  43125  hdmapfval  43150  hdmapval  43151  hgmapffval  43208  hgmapfval  43209  hgmapval  43210  resubval  43684  redivvald  43759  unxpwdom3  44363  mpaaval  44418