Theorem riotabidv 7311

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ℩cio 6440  ℩crio 7308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-uni 4859  df-iota 6442  df-riota 7309

This theorem is referenced by:  riotaeqbidv  7312  csbriota  7324  sup0riota  9357  infval  9378  ttrcltr  9613  fin23lem27  10226  subval  11358  divval  11785  flval  13700  ceilval2  13746  cjval  15011  sqrtval  15146  qnumval  16650  qdenval  16651  lubval  18262  glbval  18275  joinval2  18287  meetval2  18301  grpinvval  18895  pj1fval  19608  pj1val  19609  q1pval  26088  coeval  26156  quotval  26228  divsval  28129  ismidb  28757  lmif  28764  islmib  28766  uspgredg2v  29204  usgredg2v  29207  frgrncvvdeqlem8  30288  frgrncvvdeqlem9  30289  grpoinvval  30505  pjhval  31379  nmopadjlei  32070  cdj3lem2  32417  cvmliftlem15  35363  cvmlift2lem4  35371  cvmlift2  35381  cvmlift3lem2  35385  cvmlift3lem4  35387  cvmlift3lem6  35389  cvmlift3lem7  35390  cvmlift3lem9  35392  cvmlift3  35393  fvtransport  36097  lshpkrlem1  39229  lshpkrlem2  39230  lshpkrlem3  39231  lshpkrcl  39235  trlset  40280  trlval  40281  cdleme27b  40487  cdleme29b  40494  cdleme31so  40498  cdleme31sn1  40500  cdleme31sn1c  40507  cdleme31fv  40509  cdlemefrs29clN  40518  cdleme40v  40588  cdlemg1cN  40706  cdlemg1cex  40707  cdlemksv  40963  cdlemkuu  41014  cdlemkid3N  41052  cdlemkid4  41053  cdlemm10N  41237  dicval  41295  dihval  41351  dochfl1  41595  lcfl7N  41620  lcfrlem8  41668  lcfrlem9  41669  lcf1o  41670  mapdhval  41843  hvmapval  41879  hvmapvalvalN  41880  hdmap1fval  41915  hdmap1vallem  41916  hdmap1val  41917  hdmap1cbv  41921  hdmapfval  41946  hdmapval  41947  hgmapffval  42004  hgmapfval  42005  hgmapval  42006  resubval  42485  redivvald  42560  unxpwdom3  43212  mpaaval  43268