Theorem riotaeqbidv 7391

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-iota 6516  df-riota 7388

This theorem is referenced by:  dfoi  9549  oieq1  9550  oieq2  9551  ordtypecbv  9555  ordtypelem3  9558  zorn2lem1  10534  zorn2g  10541  cidfval  17721  cidval  17722  cidpropd  17755  lubfval  18408  glbfval  18421  grpinvfval  19009  grpinvfvalALT  19010  pj1fval  19727  mpfrcl  22127  evlsval  22128  q1pval  26209  ig1pval  26230  scutval  27860  mirval  28678  midf  28799  ismidb  28801  lmif  28808  islmib  28810  gidval  30541  grpoinvfval  30551  pjhfval  31425  cvmliftlem5  35274  cvmliftlem15  35283  weiunlem2  36446  trlfset  40143  dicffval  41157  dicfval  41158  dihffval  41213  dihfval  41214  hvmapffval  41741  hvmapfval  41742  hdmap1fval  41779  hdmapffval  41809  hdmapfval  41810  hgmapfval  41869  wessf1ornlem  45128