Theorem riotabidv 7322

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ℩cio 6446  ℩crio 7319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-uni 4846  df-iota 6448  df-riota 7320

This theorem is referenced by:  riotaeqbidv  7323  csbriota  7335  sup0riota  9376  infval  9397  ttrcltr  9635  fin23lem27  10248  subval  11382  divval  11809  flval  13751  ceilval2  13797  cjval  15062  sqrtval  15197  qnumval  16705  qdenval  16706  lubval  18318  glbval  18331  joinval2  18343  meetval2  18357  grpinvval  18954  pj1fval  19667  pj1val  19668  q1pval  26145  coeval  26213  quotval  26283  divsval  28206  ismidb  28871  lmif  28878  islmib  28880  uspgredg2v  29318  usgredg2v  29321  frgrncvvdeqlem8  30401  frgrncvvdeqlem9  30402  grpoinvval  30619  pjhval  31493  nmopadjlei  32184  cdj3lem2  32531  cvmliftlem15  35533  cvmlift2lem4  35541  cvmlift2  35551  cvmlift3lem2  35555  cvmlift3lem4  35557  cvmlift3lem6  35559  cvmlift3lem7  35560  cvmlift3lem9  35562  cvmlift3  35563  fvtransport  36267  lshpkrlem1  39609  lshpkrlem2  39610  lshpkrlem3  39611  lshpkrcl  39615  trlset  40660  trlval  40661  cdleme27b  40867  cdleme29b  40874  cdleme31so  40878  cdleme31sn1  40880  cdleme31sn1c  40887  cdleme31fv  40889  cdlemefrs29clN  40898  cdleme40v  40968  cdlemg1cN  41086  cdlemg1cex  41087  cdlemksv  41343  cdlemkuu  41394  cdlemkid3N  41432  cdlemkid4  41433  cdlemm10N  41617  dicval  41675  dihval  41731  dochfl1  41975  lcfl7N  42000  lcfrlem8  42048  lcfrlem9  42049  lcf1o  42050  mapdhval  42223  hvmapval  42259  hvmapvalvalN  42260  hdmap1fval  42295  hdmap1vallem  42296  hdmap1val  42297  hdmap1cbv  42301  hdmapfval  42326  hdmapval  42327  hgmapffval  42384  hgmapfval  42385  hgmapval  42386  resubval  42851  redivvald  42926  unxpwdom3  43547  mpaaval  43603