Theorem riotaeqbidv 7392

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539  ℩crio 7388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-uni 4907  df-iota 6513  df-riota 7389

This theorem is referenced by:  dfoi  9552  oieq1  9553  oieq2  9554  ordtypecbv  9558  ordtypelem3  9561  zorn2lem1  10537  zorn2g  10544  cidfval  17720  cidval  17721  cidpropd  17754  lubfval  18396  glbfval  18409  grpinvfval  18997  grpinvfvalALT  18998  pj1fval  19713  mpfrcl  22110  evlsval  22111  q1pval  26195  ig1pval  26216  scutval  27846  mirval  28664  midf  28785  ismidb  28787  lmif  28794  islmib  28796  gidval  30532  grpoinvfval  30542  pjhfval  31416  cvmliftlem5  35295  cvmliftlem15  35304  weiunlem2  36465  trlfset  40163  dicffval  41177  dicfval  41178  dihffval  41233  dihfval  41234  hvmapffval  41761  hvmapfval  41762  hdmap1fval  41799  hdmapffval  41829  hdmapfval  41830  hgmapfval  41889  wessf1ornlem  45195