Theorem riotabidv 7319

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ℩cio 6446  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-iota 6448  df-riota 7317

This theorem is referenced by:  riotaeqbidv  7320  csbriota  7332  sup0riota  9372  infval  9393  ttrcltr  9628  fin23lem27  10241  subval  11375  divval  11802  flval  13744  ceilval2  13790  cjval  15055  sqrtval  15190  qnumval  16698  qdenval  16699  lubval  18311  glbval  18324  joinval2  18336  meetval2  18350  grpinvval  18947  pj1fval  19660  pj1val  19661  q1pval  26130  coeval  26198  quotval  26269  divsval  28195  ismidb  28860  lmif  28867  islmib  28869  uspgredg2v  29307  usgredg2v  29310  frgrncvvdeqlem8  30391  frgrncvvdeqlem9  30392  grpoinvval  30609  pjhval  31483  nmopadjlei  32174  cdj3lem2  32521  cvmliftlem15  35496  cvmlift2lem4  35504  cvmlift2  35514  cvmlift3lem2  35518  cvmlift3lem4  35520  cvmlift3lem6  35522  cvmlift3lem7  35523  cvmlift3lem9  35525  cvmlift3  35526  fvtransport  36230  lshpkrlem1  39570  lshpkrlem2  39571  lshpkrlem3  39572  lshpkrcl  39576  trlset  40621  trlval  40622  cdleme27b  40828  cdleme29b  40835  cdleme31so  40839  cdleme31sn1  40841  cdleme31sn1c  40848  cdleme31fv  40850  cdlemefrs29clN  40859  cdleme40v  40929  cdlemg1cN  41047  cdlemg1cex  41048  cdlemksv  41304  cdlemkuu  41355  cdlemkid3N  41393  cdlemkid4  41394  cdlemm10N  41578  dicval  41636  dihval  41692  dochfl1  41936  lcfl7N  41961  lcfrlem8  42009  lcfrlem9  42010  lcf1o  42011  mapdhval  42184  hvmapval  42220  hvmapvalvalN  42221  hdmap1fval  42256  hdmap1vallem  42257  hdmap1val  42258  hdmap1cbv  42262  hdmapfval  42287  hdmapval  42288  hgmapffval  42345  hgmapfval  42346  hgmapval  42347  resubval  42813  redivvald  42888  unxpwdom3  43541  mpaaval  43597