Theorem riotaeqbidv 7407

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-iota 6525  df-riota 7404

This theorem is referenced by:  dfoi  9580  oieq1  9581  oieq2  9582  ordtypecbv  9586  ordtypelem3  9589  zorn2lem1  10565  zorn2g  10572  cidfval  17734  cidval  17735  cidpropd  17768  lubfval  18420  glbfval  18433  grpinvfval  19018  grpinvfvalALT  19019  pj1fval  19736  mpfrcl  22132  evlsval  22133  q1pval  26214  ig1pval  26235  scutval  27863  mirval  28681  midf  28802  ismidb  28804  lmif  28811  islmib  28813  gidval  30544  grpoinvfval  30554  pjhfval  31428  cvmliftlem5  35257  cvmliftlem15  35266  weiunlem2  36429  trlfset  40117  dicffval  41131  dicfval  41132  dihffval  41187  dihfval  41188  hvmapffval  41715  hvmapfval  41716  hdmap1fval  41753  hdmapffval  41783  hdmapfval  41784  hgmapfval  41843  wessf1ornlem  45092