Theorem riotaeqbidv 7306

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ℩crio 7302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-iota 6437  df-riota 7303

This theorem is referenced by:  dfoi  9397  oieq1  9398  oieq2  9399  ordtypecbv  9403  ordtypelem3  9406  zorn2lem1  10387  zorn2g  10394  cidfval  17582  cidval  17583  cidpropd  17616  lubfval  18254  glbfval  18267  grpinvfval  18891  grpinvfvalALT  18892  pj1fval  19606  mpfrcl  22020  evlsval  22021  q1pval  26087  ig1pval  26108  scutval  27741  mirval  28633  midf  28754  ismidb  28756  lmif  28763  islmib  28765  gidval  30492  grpoinvfval  30502  pjhfval  31376  cvmliftlem5  35333  cvmliftlem15  35342  weiunlem2  36507  trlfset  40258  dicffval  41272  dicfval  41273  dihffval  41328  dihfval  41329  hvmapffval  41856  hvmapfval  41857  hdmap1fval  41894  hdmapffval  41924  hdmapfval  41925  hgmapfval  41984  wessf1ornlem  45281