Theorem riotabidv 7227

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   ∈ wcel 2109  ℩cio 6386  ℩crio 7224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908  df-uni 4845  df-iota 6388  df-riota 7225

This theorem is referenced by:  riotaeqbidv  7228  csbriota  7241  sup0riota  9185  infval  9206  ttrcltr  9435  fin23lem27  10068  subval  11195  divval  11618  flval  13495  ceilval2  13541  cjval  14794  sqrtval  14929  qnumval  16422  qdenval  16423  lubval  18055  glbval  18068  joinval2  18080  meetval2  18094  grpinvval  18601  pj1fval  19281  pj1val  19282  q1pval  25299  coeval  25365  quotval  25433  ismidb  27120  lmif  27127  islmib  27129  uspgredg2v  27572  usgredg2v  27575  frgrncvvdeqlem8  28649  frgrncvvdeqlem9  28650  grpoinvval  28864  pjhval  29738  nmopadjlei  30429  cdj3lem2  30776  cvmliftlem15  33239  cvmlift2lem4  33247  cvmlift2  33257  cvmlift3lem2  33261  cvmlift3lem4  33263  cvmlift3lem6  33265  cvmlift3lem7  33266  cvmlift3lem9  33268  cvmlift3  33269  fvtransport  34313  lshpkrlem1  37103  lshpkrlem2  37104  lshpkrlem3  37105  lshpkrcl  37109  trlset  38154  trlval  38155  cdleme27b  38361  cdleme29b  38368  cdleme31so  38372  cdleme31sn1  38374  cdleme31sn1c  38381  cdleme31fv  38383  cdlemefrs29clN  38392  cdleme40v  38462  cdlemg1cN  38580  cdlemg1cex  38581  cdlemksv  38837  cdlemkuu  38888  cdlemkid3N  38926  cdlemkid4  38927  cdlemm10N  39111  dicval  39169  dihval  39225  dochfl1  39469  lcfl7N  39494  lcfrlem8  39542  lcfrlem9  39543  lcf1o  39544  mapdhval  39717  hvmapval  39753  hvmapvalvalN  39754  hdmap1fval  39789  hdmap1vallem  39790  hdmap1val  39791  hdmap1cbv  39795  hdmapfval  39820  hdmapval  39821  hgmapffval  39878  hgmapfval  39879  hgmapval  39880  resubval  40330  unxpwdom3  40900  mpaaval  40956