Theorem riotabidv 7349

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 6498	. 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-riota 7347	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-riota 7347	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3eqtr4g 2790	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ℩cio 6465  ℩crio 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875  df-iota 6467  df-riota 7347

This theorem is referenced by:  riotaeqbidv  7350  csbriota  7362  sup0riota  9424  infval  9445  ttrcltr  9676  fin23lem27  10288  subval  11419  divval  11846  flval  13763  ceilval2  13809  cjval  15075  sqrtval  15210  qnumval  16714  qdenval  16715  lubval  18322  glbval  18335  joinval2  18347  meetval2  18361  grpinvval  18919  pj1fval  19631  pj1val  19632  q1pval  26067  coeval  26135  quotval  26207  divsval  28099  ismidb  28712  lmif  28719  islmib  28721  uspgredg2v  29158  usgredg2v  29161  frgrncvvdeqlem8  30242  frgrncvvdeqlem9  30243  grpoinvval  30459  pjhval  31333  nmopadjlei  32024  cdj3lem2  32371  cvmliftlem15  35292  cvmlift2lem4  35300  cvmlift2  35310  cvmlift3lem2  35314  cvmlift3lem4  35316  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem9  35321  cvmlift3  35322  fvtransport  36027  lshpkrlem1  39110  lshpkrlem2  39111  lshpkrlem3  39112  lshpkrcl  39116  trlset  40162  trlval  40163  cdleme27b  40369  cdleme29b  40376  cdleme31so  40380  cdleme31sn1  40382  cdleme31sn1c  40389  cdleme31fv  40391  cdlemefrs29clN  40400  cdleme40v  40470  cdlemg1cN  40588  cdlemg1cex  40589  cdlemksv  40845  cdlemkuu  40896  cdlemkid3N  40934  cdlemkid4  40935  cdlemm10N  41119  dicval  41177  dihval  41233  dochfl1  41477  lcfl7N  41502  lcfrlem8  41550  lcfrlem9  41551  lcf1o  41552  mapdhval  41725  hvmapval  41761  hvmapvalvalN  41762  hdmap1fval  41797  hdmap1vallem  41798  hdmap1val  41799  hdmap1cbv  41803  hdmapfval  41828  hdmapval  41829  hgmapffval  41886  hgmapfval  41887  hgmapval  41888  resubval  42362  redivvald  42437  unxpwdom3  43091  mpaaval  43147