Theorem riotaeqbidv 7330

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)

Hypotheses

Ref	Expression
riotaeqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
riotaeqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
riotaeqbidv	⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem riotaeqbidv

Step	Hyp	Ref	Expression
1		riotaeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	riotabidv 7329	. 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
3		riotaeqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	riotaeqdv 7328	. 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥 ∈ 𝐵 𝜒))
5	2, 4	eqtrd 2772	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ℩crio 7326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866  df-iota 6458  df-riota 7327

This theorem is referenced by:  dfoi  9430  oieq1  9431  oieq2  9432  ordtypecbv  9436  ordtypelem3  9439  zorn2lem1  10420  zorn2g  10427  cidfval  17613  cidval  17614  cidpropd  17647  lubfval  18285  glbfval  18298  grpinvfval  18925  grpinvfvalALT  18926  pj1fval  19640  mpfrcl  22057  evlsval  22058  q1pval  26133  ig1pval  26154  cutsval  27793  mirval  28745  midf  28866  ismidb  28868  lmif  28875  islmib  28877  gidval  30606  grpoinvfval  30616  pjhfval  31490  cvmliftlem5  35511  cvmliftlem15  35520  weiunlem  36685  trlfset  40565  dicffval  41579  dicfval  41580  dihffval  41635  dihfval  41636  hvmapffval  42163  hvmapfval  42164  hdmap1fval  42201  hdmapffval  42231  hdmapfval  42232  hgmapfval  42291  wessf1ornlem  45573