Theorem riotabidv 6756

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ℩cio 5992  ℩crio 6753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-uni 4575  df-iota 5994  df-riota 6754

This theorem is referenced by:  riotaeqbidv  6757  csbriota  6766  sup0riota  8527  infval  8548  fin23lem27  9352  subval  10474  divval  10889  flval  12803  ceilval2  12849  cjval  14050  sqrtval  14185  qnumval  15652  qdenval  15653  lubval  17192  glbval  17205  joinval2  17217  meetval2  17231  grpinvval  17669  pj1fval  18314  pj1val  18315  q1pval  24133  coeval  24199  quotval  24267  ismidb  25891  lmif  25898  islmib  25900  uspgredg2v  26338  usgredg2v  26341  frgrncvvdeqlem8  27488  frgrncvvdeqlem9  27489  grpoinvval  27717  pjhval  28596  nmopadjlei  29287  cdj3lem2  29634  cvmliftlem15  31618  cvmlift2lem4  31626  cvmlift2  31636  cvmlift3lem2  31640  cvmlift3lem4  31642  cvmlift3lem6  31644  cvmlift3lem7  31645  cvmlift3lem9  31647  cvmlift3  31648  fvtransport  32476  lshpkrlem1  34919  lshpkrlem2  34920  lshpkrlem3  34921  lshpkrcl  34925  trlset  35970  trlval  35971  cdleme27b  36177  cdleme29b  36184  cdleme31so  36188  cdleme31sn1  36190  cdleme31sn1c  36197  cdleme31fv  36199  cdlemefrs29clN  36208  cdleme40v  36278  cdlemg1cN  36396  cdlemg1cex  36397  cdlemksv  36653  cdlemkuu  36704  cdlemkid3N  36742  cdlemkid4  36743  cdlemm10N  36928  dicval  36986  dihval  37042  dochfl1  37286  lcfl7N  37311  lcfrlem8  37359  lcfrlem9  37360  lcf1o  37361  mapdhval  37534  hvmapval  37570  hvmapvalvalN  37571  hdmap1fval  37606  hdmap1vallem  37607  hdmap1val  37608  hdmap1cbv  37612  hdmapfval  37637  hdmapval  37638  hgmapffval  37695  hgmapfval  37696  hgmapval  37697  unxpwdom3  38191  mpaaval  38247