Theorem riotaeqbidv 7316

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

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

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 3429  df-ss 3902  df-uni 4841  df-iota 6443  df-riota 7313

This theorem is referenced by:  dfoi  9415  oieq1  9416  oieq2  9417  ordtypecbv  9421  ordtypelem3  9424  zorn2lem1  10407  zorn2g  10414  cidfval  17631  cidval  17632  cidpropd  17665  lubfval  18303  glbfval  18316  grpinvfval  18943  grpinvfvalALT  18944  pj1fval  19658  mpfrcl  22052  evlsval  22053  q1pval  26108  ig1pval  26129  cutsval  27760  mirval  28711  midf  28832  ismidb  28834  lmif  28841  islmib  28843  gidval  30571  grpoinvfval  30581  pjhfval  31455  cvmliftlem5  35459  cvmliftlem15  35468  weiunlem  36633  trlfset  40594  dicffval  41608  dicfval  41609  dihffval  41664  dihfval  41665  hvmapffval  42192  hvmapfval  42193  hdmap1fval  42230  hdmapffval  42260  hdmapfval  42261  hgmapfval  42320  wessf1ornlem  45603