Theorem riotaeqbidv 7318

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863  df-iota 6447  df-riota 7315

This theorem is referenced by:  dfoi  9418  oieq1  9419  oieq2  9420  ordtypecbv  9424  ordtypelem3  9427  zorn2lem1  10408  zorn2g  10415  cidfval  17601  cidval  17602  cidpropd  17635  lubfval  18273  glbfval  18286  grpinvfval  18910  grpinvfvalALT  18911  pj1fval  19625  mpfrcl  22042  evlsval  22043  q1pval  26118  ig1pval  26139  scutval  27776  mirval  28708  midf  28829  ismidb  28831  lmif  28838  islmib  28840  gidval  30568  grpoinvfval  30578  pjhfval  31452  cvmliftlem5  35462  cvmliftlem15  35471  weiunlem2  36636  trlfset  40455  dicffval  41469  dicfval  41470  dihffval  41525  dihfval  41526  hvmapffval  42053  hvmapfval  42054  hdmap1fval  42091  hdmapffval  42121  hdmapfval  42122  hgmapfval  42181  wessf1ornlem  45466