Theorem riotabidv 7317

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ℩cio 6446  ℩crio 7314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864  df-iota 6448  df-riota 7315

This theorem is referenced by:  riotaeqbidv  7318  csbriota  7330  sup0riota  9369  infval  9390  ttrcltr  9625  fin23lem27  10238  subval  11371  divval  11798  flval  13714  ceilval2  13760  cjval  15025  sqrtval  15160  qnumval  16664  qdenval  16665  lubval  18277  glbval  18290  joinval2  18302  meetval2  18316  grpinvval  18910  pj1fval  19623  pj1val  19624  q1pval  26116  coeval  26184  quotval  26256  divsval  28185  ismidb  28850  lmif  28857  islmib  28859  uspgredg2v  29297  usgredg2v  29300  frgrncvvdeqlem8  30381  frgrncvvdeqlem9  30382  grpoinvval  30598  pjhval  31472  nmopadjlei  32163  cdj3lem2  32510  cvmliftlem15  35492  cvmlift2lem4  35500  cvmlift2  35510  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3lem6  35518  cvmlift3lem7  35519  cvmlift3lem9  35521  cvmlift3  35522  fvtransport  36226  lshpkrlem1  39366  lshpkrlem2  39367  lshpkrlem3  39368  lshpkrcl  39372  trlset  40417  trlval  40418  cdleme27b  40624  cdleme29b  40631  cdleme31so  40635  cdleme31sn1  40637  cdleme31sn1c  40644  cdleme31fv  40646  cdlemefrs29clN  40655  cdleme40v  40725  cdlemg1cN  40843  cdlemg1cex  40844  cdlemksv  41100  cdlemkuu  41151  cdlemkid3N  41189  cdlemkid4  41190  cdlemm10N  41374  dicval  41432  dihval  41488  dochfl1  41732  lcfl7N  41757  lcfrlem8  41805  lcfrlem9  41806  lcf1o  41807  mapdhval  41980  hvmapval  42016  hvmapvalvalN  42017  hdmap1fval  42052  hdmap1vallem  42053  hdmap1val  42054  hdmap1cbv  42058  hdmapfval  42083  hdmapval  42084  hgmapffval  42141  hgmapfval  42142  hgmapval  42143  resubval  42618  redivvald  42693  unxpwdom3  43333  mpaaval  43389