Theorem riotaeqbidv 7215

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ℩crio 7211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-iota 6376  df-riota 7212

This theorem is referenced by:  dfoi  9200  oieq1  9201  oieq2  9202  ordtypecbv  9206  ordtypelem3  9209  zorn2lem1  10183  zorn2g  10190  cidfval  17302  cidval  17303  cidpropd  17336  lubfval  17983  glbfval  17996  grpinvfval  18533  grpinvfvalALT  18534  pj1fval  19215  mpfrcl  21205  evlsval  21206  q1pval  25223  ig1pval  25242  mirval  26920  midf  27041  ismidb  27043  lmif  27050  islmib  27052  gidval  28775  grpoinvfval  28785  pjhfval  29659  cvmliftlem5  33151  cvmliftlem15  33160  scutval  33921  trlfset  38101  dicffval  39115  dicfval  39116  dihffval  39171  dihfval  39172  hvmapffval  39699  hvmapfval  39700  hdmap1fval  39737  hdmapffval  39767  hdmapfval  39768  hgmapfval  39827  wessf1ornlem  42611