Theorem riotabidv 7172

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ℩cio 6336  ℩crio 7169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-iota 6338  df-riota 7170

This theorem is referenced by:  riotaeqbidv  7173  csbriota  7186  sup0riota  9081  infval  9102  fin23lem27  9942  subval  11069  divval  11492  flval  13369  ceilval2  13415  cjval  14665  sqrtval  14800  qnumval  16293  qdenval  16294  lubval  17862  glbval  17875  joinval2  17887  meetval2  17901  grpinvval  18408  pj1fval  19084  pj1val  19085  q1pval  25051  coeval  25117  quotval  25185  ismidb  26869  lmif  26876  islmib  26878  uspgredg2v  27312  usgredg2v  27315  frgrncvvdeqlem8  28389  frgrncvvdeqlem9  28390  grpoinvval  28604  pjhval  29478  nmopadjlei  30169  cdj3lem2  30516  cvmliftlem15  32973  cvmlift2lem4  32981  cvmlift2  32991  cvmlift3lem2  32995  cvmlift3lem4  32997  cvmlift3lem6  32999  cvmlift3lem7  33000  cvmlift3lem9  33002  cvmlift3  33003  ttrcltr  33515  fvtransport  34071  lshpkrlem1  36861  lshpkrlem2  36862  lshpkrlem3  36863  lshpkrcl  36867  trlset  37912  trlval  37913  cdleme27b  38119  cdleme29b  38126  cdleme31so  38130  cdleme31sn1  38132  cdleme31sn1c  38139  cdleme31fv  38141  cdlemefrs29clN  38150  cdleme40v  38220  cdlemg1cN  38338  cdlemg1cex  38339  cdlemksv  38595  cdlemkuu  38646  cdlemkid3N  38684  cdlemkid4  38685  cdlemm10N  38869  dicval  38927  dihval  38983  dochfl1  39227  lcfl7N  39252  lcfrlem8  39300  lcfrlem9  39301  lcf1o  39302  mapdhval  39475  hvmapval  39511  hvmapvalvalN  39512  hdmap1fval  39547  hdmap1vallem  39548  hdmap1val  39549  hdmap1cbv  39553  hdmapfval  39578  hdmapval  39579  hgmapffval  39636  hgmapfval  39637  hgmapval  39638  resubval  40058  unxpwdom3  40623  mpaaval  40679