Theorem riotaeqbidv 7374

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  ℩crio 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-v 3464  df-ss 3930  df-uni 4878  df-iota 6496  df-riota 7371

This theorem is referenced by:  dfoi  9476  oieq1  9477  oieq2  9478  ordtypecbv  9482  ordtypelem3  9485  zorn2lem1  10483  zorn2g  10490  cidfval  17735  cidval  17736  cidpropd  17769  lubfval  18407  glbfval  18420  grpinvfval  19048  grpinvfvalALT  19049  pj1fval  19767  mpfrcl  22219  evlsval  22220  q1pval  26295  ig1pval  26316  cutsval  27953  mirval  28912  midf  29063  ismidb  29065  lmif  29072  islmib  29074  gidval  30834  grpoinvfval  30844  pjhfval  31718  cvmliftlem5  35739  cvmliftlem15  35748  weiunlem  36922  trlfset  40884  dicffval  41898  dicfval  41899  dihffval  41954  dihfval  41955  hvmapffval  42482  hvmapfval  42483  hdmap1fval  42520  hdmapffval  42550  hdmapfval  42551  hgmapfval  42610  wessf1ornlem  45855