Theorem riotabidv 6847

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2157  ℩cio 6072  ℩crio 6844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rex 3113  df-uni 4642  df-iota 6074  df-riota 6845

This theorem is referenced by:  riotaeqbidv  6848  csbriota  6857  sup0riota  8620  infval  8641  fin23lem27  9445  subval  10567  divval  10982  flval  12839  ceilval2  12885  cjval  14085  sqrtval  14220  qnumval  15682  qdenval  15683  lubval  17209  glbval  17222  joinval2  17234  meetval2  17248  grpinvval  17686  pj1fval  18328  pj1val  18329  q1pval  24150  coeval  24216  quotval  24284  ismidb  25907  lmif  25914  islmib  25916  uspgredg2v  26354  usgredg2v  26357  frgrncvvdeqlem8  27504  frgrncvvdeqlem9  27505  grpoinvval  27729  pjhval  28607  nmopadjlei  29298  cdj3lem2  29645  cvmliftlem15  31625  cvmlift2lem4  31633  cvmlift2  31643  cvmlift3lem2  31647  cvmlift3lem4  31649  cvmlift3lem6  31651  cvmlift3lem7  31652  cvmlift3lem9  31654  cvmlift3  31655  fvtransport  32482  lshpkrlem1  34909  lshpkrlem2  34910  lshpkrlem3  34911  lshpkrcl  34915  trlset  35960  trlval  35961  cdleme27b  36167  cdleme29b  36174  cdleme31so  36178  cdleme31sn1  36180  cdleme31sn1c  36187  cdleme31fv  36189  cdlemefrs29clN  36198  cdleme40v  36268  cdlemg1cN  36386  cdlemg1cex  36387  cdlemksv  36643  cdlemkuu  36694  cdlemkid3N  36732  cdlemkid4  36733  cdlemm10N  36917  dicval  36975  dihval  37031  dochfl1  37275  lcfl7N  37300  lcfrlem8  37348  lcfrlem9  37349  lcf1o  37350  mapdhval  37523  hvmapval  37559  hvmapvalvalN  37560  hdmap1fval  37595  hdmap1vallem  37596  hdmap1val  37597  hdmap1cbv  37601  hdmapfval  37626  hdmapval  37627  hgmapffval  37684  hgmapfval  37685  hgmapval  37686  unxpwdom3  38184  mpaaval  38240