Theorem riotabidv 7346

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872  df-iota 6464  df-riota 7344

This theorem is referenced by:  riotaeqbidv  7347  csbriota  7359  sup0riota  9417  infval  9438  ttrcltr  9669  fin23lem27  10281  subval  11412  divval  11839  flval  13756  ceilval2  13802  cjval  15068  sqrtval  15203  qnumval  16707  qdenval  16708  lubval  18315  glbval  18328  joinval2  18340  meetval2  18354  grpinvval  18912  pj1fval  19624  pj1val  19625  q1pval  26060  coeval  26128  quotval  26200  divsval  28092  ismidb  28705  lmif  28712  islmib  28714  uspgredg2v  29151  usgredg2v  29154  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  grpoinvval  30452  pjhval  31326  nmopadjlei  32017  cdj3lem2  32364  cvmliftlem15  35285  cvmlift2lem4  35293  cvmlift2  35303  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  cvmlift3  35315  fvtransport  36020  lshpkrlem1  39103  lshpkrlem2  39104  lshpkrlem3  39105  lshpkrcl  39109  trlset  40155  trlval  40156  cdleme27b  40362  cdleme29b  40369  cdleme31so  40373  cdleme31sn1  40375  cdleme31sn1c  40382  cdleme31fv  40384  cdlemefrs29clN  40393  cdleme40v  40463  cdlemg1cN  40581  cdlemg1cex  40582  cdlemksv  40838  cdlemkuu  40889  cdlemkid3N  40927  cdlemkid4  40928  cdlemm10N  41112  dicval  41170  dihval  41226  dochfl1  41470  lcfl7N  41495  lcfrlem8  41543  lcfrlem9  41544  lcf1o  41545  mapdhval  41718  hvmapval  41754  hvmapvalvalN  41755  hdmap1fval  41790  hdmap1vallem  41791  hdmap1val  41792  hdmap1cbv  41796  hdmapfval  41821  hdmapval  41822  hgmapffval  41879  hgmapfval  41880  hgmapval  41881  resubval  42355  redivvald  42430  unxpwdom3  43084  mpaaval  43140