Theorem riotabidv 6613

Description: Formula-building deduction rule 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 740	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	iotabidv 5872	. 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-riota 6611	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-riota 6611	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3eqtr4g 2681	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ℩cio 5849  ℩crio 6610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-iota 5851  df-riota 6611

This theorem is referenced by:  riotaeqbidv  6614  csbriota  6623  sup0riota  8371  infval  8392  fin23lem27  9150  subval  10272  divval  10687  flval  12595  ceilval2  12641  cjval  13842  sqrtval  13977  qnumval  15445  qdenval  15446  lubval  16984  glbval  16997  joinval2  17009  meetval2  17023  grpinvval  17461  pj1fval  18107  pj1val  18108  q1pval  23913  coeval  23979  quotval  24047  ismidb  25670  lmif  25677  islmib  25679  uspgredg2v  26116  usgredg2v  26119  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  grpoinvval  27377  pjhval  28256  nmopadjlei  28947  cdj3lem2  29294  cvmliftlem15  31280  cvmlift2lem4  31288  cvmlift2  31298  cvmlift3lem2  31302  cvmlift3lem4  31304  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  cvmlift3  31310  fvtransport  32139  lshpkrlem1  34397  lshpkrlem2  34398  lshpkrlem3  34399  lshpkrcl  34403  trlset  35448  trlval  35449  cdleme27b  35656  cdleme29b  35663  cdleme31so  35667  cdleme31sn1  35669  cdleme31sn1c  35676  cdleme31fv  35678  cdlemefrs29clN  35687  cdleme40v  35757  cdlemg1cN  35875  cdlemg1cex  35876  cdlemksv  36132  cdlemkuu  36183  cdlemkid3N  36221  cdlemkid4  36222  cdlemm10N  36407  dicval  36465  dihval  36521  dochfl1  36765  lcfl7N  36790  lcfrlem8  36838  lcfrlem9  36839  lcf1o  36840  mapdhval  37013  hvmapval  37049  hvmapvalvalN  37050  hdmap1fval  37086  hdmap1vallem  37087  hdmap1val  37088  hdmap1cbv  37092  hdmapfval  37119  hdmapval  37120  hgmapffval  37177  hgmapfval  37178  hgmapval  37179  unxpwdom3  37665  mpaaval  37721