Theorem riotabidv 7380

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ℩cio 6492  ℩crio 7377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-iota 6494  df-riota 7378

This theorem is used by:  riotaeqbidv  7381  csbriota  7393  sup0riota  9462  infval  9483  ttrcltr  9721  fin23lem27  10410  subval  11552  divval  11980  flval  13938  ceilval2  13984  cjval  15275  sqrtval  15410  qnumval  16919  qdenval  16920  lubval  18534  glbval  18547  joinval2  18559  meetval2  18573  grpinvval  19197  pj1fval  19914  pj1val  19915  q1pval  26479  coeval  26548  quotval  26619  divsval  28581  ismidb  29289  lmif  29296  islmib  29298  uspgredg2v  29811  usgredg2v  29814  frgrncvvdeqlem8  30913  frgrncvvdeqlem9  30914  grpoinvval  31131  pjhval  32005  nmopadjlei  32696  cdj3lem2  33043  cvmliftlem15  36150  cvmlift2lem4  36158  cvmlift2  36168  cvmlift3lem2  36172  cvmlift3lem4  36174  cvmlift3lem6  36176  cvmlift3lem7  36177  cvmlift3lem9  36179  cvmlift3  36180  fvtransport  36890  lshpkrlem1  40261  lshpkrlem2  40262  lshpkrlem3  40263  lshpkrcl  40267  trlset  41312  trlval  41313  cdleme27b  41519  cdleme29b  41526  cdleme31so  41530  cdleme31sn1  41532  cdleme31sn1c  41539  cdleme31fv  41541  cdlemefrs29clN  41550  cdleme40v  41620  cdlemg1cN  41738  cdlemg1cex  41739  cdlemksv  41995  cdlemkuu  42046  cdlemkid3N  42084  cdlemkid4  42085  cdlemm10N  42269  dicval  42327  dihval  42383  dochfl1  42627  lcfl7N  42652  lcfrlem8  42700  lcfrlem9  42701  lcf1o  42702  mapdhval  42875  hvmapval  42911  hvmapvalvalN  42912  hdmap1fval  42947  hdmap1vallem  42948  hdmap1val  42949  hdmap1cbv  42953  hdmapfval  42978  hdmapval  42979  hgmapffval  43036  hgmapfval  43037  hgmapval  43038  resubval  43512  redivvald  43587  unxpwdom3  44191  mpaaval  44247