Theorem riotaeqbidv 7380

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ℩crio 7376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868  df-iota 6494  df-riota 7377

This theorem is used by:  dfoi  9505  oieq1  9506  oieq2  9507  ordtypecbv  9511  ordtypelem3  9514  zorn2lem1  10574  zorn2g  10581  cidfval  17850  cidval  17851  cidpropd  17884  lubfval  18522  glbfval  18535  grpinvfval  19189  grpinvfvalALT  19190  pj1fval  19908  mpfrcl  22394  evlsval  22395  q1pval  26473  ig1pval  26494  cutsval  28166  mirval  29127  midf  29281  ismidb  29283  lmif  29290  islmib  29292  angmgmval  29394  gidval  31114  grpoinvfval  31124  pjhfval  31998  cvmliftlem5  36054  cvmliftlem15  36063  weiunlem  37251  trlfset  41217  dicffval  42231  dicfval  42232  dihffval  42287  dihfval  42288  hvmapffval  42815  hvmapfval  42816  hdmap1fval  42853  hdmapffval  42883  hdmapfval  42884  hgmapfval  42943  wessf1ornlem  46199