Theorem riotabidv 7371

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ℩cio 6492  ℩crio 7368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-uni 4874  df-iota 6494  df-riota 7369

This theorem is referenced by:  riotaeqbidv  7372  csbriota  7384  sup0riota  9427  infval  9448  ttrcltr  9686  fin23lem27  10313  subval  11449  divval  11875  flval  13829  ceilval2  13875  cjval  15155  sqrtval  15290  qnumval  16797  qdenval  16798  lubval  18411  glbval  18424  joinval2  18436  meetval2  18450  grpinvval  19048  pj1fval  19765  pj1val  19766  q1pval  26293  coeval  26361  quotval  26434  divsval  28363  ismidb  29068  lmif  29075  islmib  29077  uspgredg2v  29555  usgredg2v  29558  frgrncvvdeqlem8  30638  frgrncvvdeqlem9  30639  grpoinvval  30856  pjhval  31730  nmopadjlei  32421  cdj3lem2  32768  cvmliftlem15  35771  cvmlift2lem4  35779  cvmlift2  35789  cvmlift3lem2  35793  cvmlift3lem4  35795  cvmlift3lem6  35797  cvmlift3lem7  35798  cvmlift3lem9  35800  cvmlift3  35801  fvtransport  36505  lshpkrlem1  39865  lshpkrlem2  39866  lshpkrlem3  39867  lshpkrcl  39871  trlset  40916  trlval  40917  cdleme27b  41123  cdleme29b  41130  cdleme31so  41134  cdleme31sn1  41136  cdleme31sn1c  41143  cdleme31fv  41145  cdlemefrs29clN  41154  cdleme40v  41224  cdlemg1cN  41342  cdlemg1cex  41343  cdlemksv  41599  cdlemkuu  41650  cdlemkid3N  41688  cdlemkid4  41689  cdlemm10N  41873  dicval  41931  dihval  41987  dochfl1  42231  lcfl7N  42256  lcfrlem8  42304  lcfrlem9  42305  lcf1o  42306  mapdhval  42479  hvmapval  42515  hvmapvalvalN  42516  hdmap1fval  42551  hdmap1vallem  42552  hdmap1val  42553  hdmap1cbv  42557  hdmapfval  42582  hdmapval  42583  hgmapffval  42640  hgmapfval  42641  hgmapval  42642  resubval  43109  redivvald  43184  unxpwdom3  43805  mpaaval  43861