Theorem riotabidv 6937

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ℩cio 6147  ℩crio 6934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-rex 3088  df-uni 4709  df-iota 6149  df-riota 6935

This theorem is referenced by:  riotaeqbidv  6938  csbriota  6947  sup0riota  8722  infval  8743  fin23lem27  9546  subval  10675  divval  11099  flval  12977  ceilval2  13023  cjval  14320  sqrtval  14455  qnumval  15931  qdenval  15932  lubval  17464  glbval  17477  joinval2  17489  meetval2  17503  grpinvval  17943  pj1fval  18590  pj1val  18591  q1pval  24462  coeval  24528  quotval  24596  ismidb  26278  lmif  26285  islmib  26287  uspgredg2v  26721  usgredg2v  26724  frgrncvvdeqlem8  27852  frgrncvvdeqlem9  27853  grpoinvval  28089  pjhval  28967  nmopadjlei  29658  cdj3lem2  30005  cvmliftlem15  32159  cvmlift2lem4  32167  cvmlift2  32177  cvmlift3lem2  32181  cvmlift3lem4  32183  cvmlift3lem6  32185  cvmlift3lem7  32186  cvmlift3lem9  32188  cvmlift3  32189  fvtransport  33043  lshpkrlem1  35720  lshpkrlem2  35721  lshpkrlem3  35722  lshpkrcl  35726  trlset  36771  trlval  36772  cdleme27b  36978  cdleme29b  36985  cdleme31so  36989  cdleme31sn1  36991  cdleme31sn1c  36998  cdleme31fv  37000  cdlemefrs29clN  37009  cdleme40v  37079  cdlemg1cN  37197  cdlemg1cex  37198  cdlemksv  37454  cdlemkuu  37505  cdlemkid3N  37543  cdlemkid4  37544  cdlemm10N  37728  dicval  37786  dihval  37842  dochfl1  38086  lcfl7N  38111  lcfrlem8  38159  lcfrlem9  38160  lcf1o  38161  mapdhval  38334  hvmapval  38370  hvmapvalvalN  38371  hdmap1fval  38406  hdmap1vallem  38407  hdmap1val  38408  hdmap1cbv  38412  hdmapfval  38437  hdmapval  38438  hgmapffval  38495  hgmapfval  38496  hgmapval  38497  resubval  38658  unxpwdom3  39120  mpaaval  39176