Theorem riotabidv 7369

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ℩cio 6492  ℩crio 7366

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-iota 6494  df-riota 7367

This theorem is referenced by:  riotaeqbidv  7370  csbriota  7383  sup0riota  9462  infval  9483  ttrcltr  9713  fin23lem27  10325  subval  11455  divval  11878  flval  13763  ceilval2  13809  cjval  15053  sqrtval  15188  qnumval  16677  qdenval  16678  lubval  18313  glbval  18326  joinval2  18338  meetval2  18352  grpinvval  18901  pj1fval  19603  pj1val  19604  q1pval  25906  coeval  25972  quotval  26041  divsval  27876  ismidb  28296  lmif  28303  islmib  28305  uspgredg2v  28748  usgredg2v  28751  frgrncvvdeqlem8  29826  frgrncvvdeqlem9  29827  grpoinvval  30043  pjhval  30917  nmopadjlei  31608  cdj3lem2  31955  cvmliftlem15  34587  cvmlift2lem4  34595  cvmlift2  34605  cvmlift3lem2  34609  cvmlift3lem4  34611  cvmlift3lem6  34613  cvmlift3lem7  34614  cvmlift3lem9  34616  cvmlift3  34617  fvtransport  35308  lshpkrlem1  38283  lshpkrlem2  38284  lshpkrlem3  38285  lshpkrcl  38289  trlset  39335  trlval  39336  cdleme27b  39542  cdleme29b  39549  cdleme31so  39553  cdleme31sn1  39555  cdleme31sn1c  39562  cdleme31fv  39564  cdlemefrs29clN  39573  cdleme40v  39643  cdlemg1cN  39761  cdlemg1cex  39762  cdlemksv  40018  cdlemkuu  40069  cdlemkid3N  40107  cdlemkid4  40108  cdlemm10N  40292  dicval  40350  dihval  40406  dochfl1  40650  lcfl7N  40675  lcfrlem8  40723  lcfrlem9  40724  lcf1o  40725  mapdhval  40898  hvmapval  40934  hvmapvalvalN  40935  hdmap1fval  40970  hdmap1vallem  40971  hdmap1val  40972  hdmap1cbv  40976  hdmapfval  41001  hdmapval  41002  hgmapffval  41059  hgmapfval  41060  hgmapval  41061  resubval  41542  unxpwdom3  42139  mpaaval  42195