Theorem riotabidv 7266

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ∈ wcel 2104  ℩cio 6408  ℩crio 7263

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 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909  df-uni 4845  df-iota 6410  df-riota 7264

This theorem is referenced by:  riotaeqbidv  7267  csbriota  7280  sup0riota  9268  infval  9289  ttrcltr  9518  fin23lem27  10130  subval  11258  divval  11681  flval  13560  ceilval2  13606  cjval  14858  sqrtval  14993  qnumval  16486  qdenval  16487  lubval  18119  glbval  18132  joinval2  18144  meetval2  18158  grpinvval  18665  pj1fval  19345  pj1val  19346  q1pval  25363  coeval  25429  quotval  25497  ismidb  27184  lmif  27191  islmib  27193  uspgredg2v  27636  usgredg2v  27639  frgrncvvdeqlem8  28715  frgrncvvdeqlem9  28716  grpoinvval  28930  pjhval  29804  nmopadjlei  30495  cdj3lem2  30842  cvmliftlem15  33305  cvmlift2lem4  33313  cvmlift2  33323  cvmlift3lem2  33327  cvmlift3lem4  33329  cvmlift3lem6  33331  cvmlift3lem7  33332  cvmlift3lem9  33334  cvmlift3  33335  fvtransport  34379  lshpkrlem1  37166  lshpkrlem2  37167  lshpkrlem3  37168  lshpkrcl  37172  trlset  38217  trlval  38218  cdleme27b  38424  cdleme29b  38431  cdleme31so  38435  cdleme31sn1  38437  cdleme31sn1c  38444  cdleme31fv  38446  cdlemefrs29clN  38455  cdleme40v  38525  cdlemg1cN  38643  cdlemg1cex  38644  cdlemksv  38900  cdlemkuu  38951  cdlemkid3N  38989  cdlemkid4  38990  cdlemm10N  39174  dicval  39232  dihval  39288  dochfl1  39532  lcfl7N  39557  lcfrlem8  39605  lcfrlem9  39606  lcf1o  39607  mapdhval  39780  hvmapval  39816  hvmapvalvalN  39817  hdmap1fval  39852  hdmap1vallem  39853  hdmap1val  39854  hdmap1cbv  39858  hdmapfval  39883  hdmapval  39884  hgmapffval  39941  hgmapfval  39942  hgmapval  39943  resubval  40387  unxpwdom3  40958  mpaaval  41014