Theorem riotaeqbidv 7329

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 7328	. 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒))
3		riotaeqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	riotaeqdv 7327	. 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥 ∈ 𝐵 𝜒))
5	2, 4	eqtrd 2764	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ℩crio 7325

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 3446  df-ss 3928  df-uni 4868  df-iota 6452  df-riota 7326

This theorem is referenced by:  dfoi  9440  oieq1  9441  oieq2  9442  ordtypecbv  9446  ordtypelem3  9449  zorn2lem1  10425  zorn2g  10432  cidfval  17617  cidval  17618  cidpropd  17651  lubfval  18289  glbfval  18302  grpinvfval  18892  grpinvfvalALT  18893  pj1fval  19608  mpfrcl  22025  evlsval  22026  q1pval  26093  ig1pval  26114  scutval  27746  mirval  28635  midf  28756  ismidb  28758  lmif  28765  islmib  28767  gidval  30491  grpoinvfval  30501  pjhfval  31375  cvmliftlem5  35269  cvmliftlem15  35278  weiunlem2  36444  trlfset  40147  dicffval  41161  dicfval  41162  dihffval  41217  dihfval  41218  hvmapffval  41745  hvmapfval  41746  hdmap1fval  41783  hdmapffval  41813  hdmapfval  41814  hgmapfval  41873  wessf1ornlem  45172