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  10427  zorn2g  10434  cidfval  17618  cidval  17619  cidpropd  17652  lubfval  18290  glbfval  18303  grpinvfval  18893  grpinvfvalALT  18894  pj1fval  19609  mpfrcl  22026  evlsval  22027  q1pval  26094  ig1pval  26115  scutval  27747  mirval  28636  midf  28757  ismidb  28759  lmif  28766  islmib  28768  gidval  30492  grpoinvfval  30502  pjhfval  31376  cvmliftlem5  35270  cvmliftlem15  35279  weiunlem2  36445  trlfset  40148  dicffval  41162  dicfval  41163  dihffval  41218  dihfval  41219  hvmapffval  41746  hvmapfval  41747  hdmap1fval  41784  hdmapffval  41814  hdmapfval  41815  hgmapfval  41874  wessf1ornlem  45173