Theorem riotaeqbidv 7372

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872  df-iota 6492  df-riota 7369

This theorem is used by:  dfoi  9471  oieq1  9472  oieq2  9473  ordtypecbv  9477  ordtypelem3  9480  zorn2lem1  10486  zorn2g  10493  cidfval  17738  cidval  17739  cidpropd  17772  lubfval  18410  glbfval  18423  grpinvfval  19051  grpinvfvalALT  19052  pj1fval  19770  mpfrcl  22247  evlsval  22248  q1pval  26323  ig1pval  26344  cutsval  27984  mirval  28943  midf  29096  ismidb  29098  lmif  29105  islmib  29107  gidval  30875  grpoinvfval  30885  pjhfval  31759  cvmliftlem5  35789  cvmliftlem15  35798  weiunlem  37002  trlfset  40962  dicffval  41976  dicfval  41977  dihffval  42032  dihfval  42033  hvmapffval  42560  hvmapfval  42561  hdmap1fval  42598  hdmapffval  42628  hdmapfval  42629  hgmapfval  42688  wessf1ornlem  45931