Theorem riotaeqbidv 7320

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842  df-iota 6445  df-riota 7317

This theorem is referenced by:  dfoi  9420  oieq1  9421  oieq2  9422  ordtypecbv  9426  ordtypelem3  9429  zorn2lem1  10413  zorn2g  10420  cidfval  17637  cidval  17638  cidpropd  17671  lubfval  18309  glbfval  18322  grpinvfval  18949  grpinvfvalALT  18950  pj1fval  19664  mpfrcl  22065  evlsval  22066  q1pval  26142  ig1pval  26163  cutsval  27794  mirval  28745  midf  28866  ismidb  28868  lmif  28875  islmib  28877  gidval  30605  grpoinvfval  30615  pjhfval  31489  cvmliftlem5  35532  cvmliftlem15  35541  weiunlem  36706  trlfset  40667  dicffval  41681  dicfval  41682  dihffval  41737  dihfval  41738  hvmapffval  42265  hvmapfval  42266  hdmap1fval  42303  hdmapffval  42333  hdmapfval  42334  hgmapfval  42393  wessf1ornlem  45646