Theorem riotaeqbidv 7400

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-iota 6509  df-riota 7397

This theorem is used by:  dfoi  9529  oieq1  9530  oieq2  9531  ordtypecbv  9535  ordtypelem3  9538  zorn2lem1  10598  zorn2g  10605  cidfval  17876  cidval  17877  cidpropd  17910  lubfval  18548  glbfval  18561  grpinvfval  19215  grpinvfvalALT  19216  pj1fval  19935  mpfrcl  22421  evlsval  22422  q1pval  26500  ig1pval  26521  cutsval  28193  mirval  29154  midf  29308  ismidb  29310  lmif  29317  islmib  29319  angmgmval  29421  gidval  31141  grpoinvfval  31151  pjhfval  32025  cvmliftlem5  36220  cvmliftlem15  36229  weiunlem  37428  trlfset  41408  dicffval  42422  dicfval  42423  dihffval  42478  dihfval  42479  hvmapffval  43006  hvmapfval  43007  hdmap1fval  43044  hdmapffval  43074  hdmapfval  43075  hgmapfval  43134  wessf1ornlem  46403