Theorem riotabidv 7364

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ℩cio 6482  ℩crio 7361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-iota 6484  df-riota 7362

This theorem is referenced by:  riotaeqbidv  7365  csbriota  7377  sup0riota  9478  infval  9499  ttrcltr  9730  fin23lem27  10342  subval  11473  divval  11898  flval  13811  ceilval2  13857  cjval  15121  sqrtval  15256  qnumval  16756  qdenval  16757  lubval  18366  glbval  18379  joinval2  18391  meetval2  18405  grpinvval  18963  pj1fval  19675  pj1val  19676  q1pval  26112  coeval  26180  quotval  26252  divsval  28144  ismidb  28757  lmif  28764  islmib  28766  uspgredg2v  29203  usgredg2v  29206  frgrncvvdeqlem8  30287  frgrncvvdeqlem9  30288  grpoinvval  30504  pjhval  31378  nmopadjlei  32069  cdj3lem2  32416  cvmliftlem15  35320  cvmlift2lem4  35328  cvmlift2  35338  cvmlift3lem2  35342  cvmlift3lem4  35344  cvmlift3lem6  35346  cvmlift3lem7  35347  cvmlift3lem9  35349  cvmlift3  35350  fvtransport  36050  lshpkrlem1  39128  lshpkrlem2  39129  lshpkrlem3  39130  lshpkrcl  39134  trlset  40180  trlval  40181  cdleme27b  40387  cdleme29b  40394  cdleme31so  40398  cdleme31sn1  40400  cdleme31sn1c  40407  cdleme31fv  40409  cdlemefrs29clN  40418  cdleme40v  40488  cdlemg1cN  40606  cdlemg1cex  40607  cdlemksv  40863  cdlemkuu  40914  cdlemkid3N  40952  cdlemkid4  40953  cdlemm10N  41137  dicval  41195  dihval  41251  dochfl1  41495  lcfl7N  41520  lcfrlem8  41568  lcfrlem9  41569  lcf1o  41570  mapdhval  41743  hvmapval  41779  hvmapvalvalN  41780  hdmap1fval  41815  hdmap1vallem  41816  hdmap1val  41817  hdmap1cbv  41821  hdmapfval  41846  hdmapval  41847  hgmapffval  41904  hgmapfval  41905  hgmapval  41906  resubval  42410  unxpwdom3  43119  mpaaval  43175