Theorem riotaeqbidv 7376

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ℩crio 7372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871  df-iota 6493  df-riota 7373

This theorem is used by:  dfoi  9486  oieq1  9487  oieq2  9488  ordtypecbv  9492  ordtypelem3  9495  zorn2lem1  10501  zorn2g  10508  cidfval  17768  cidval  17769  cidpropd  17802  lubfval  18440  glbfval  18453  grpinvfval  19103  grpinvfvalALT  19104  pj1fval  19822  mpfrcl  22302  evlsval  22303  q1pval  26382  ig1pval  26403  cutsval  28043  mirval  29004  midf  29158  ismidb  29160  lmif  29167  islmib  29169  gidval  30979  grpoinvfval  30989  pjhfval  31863  cvmliftlem5  35855  cvmliftlem15  35864  weiunlem  37069  trlfset  41020  dicffval  42034  dicfval  42035  dihffval  42090  dihfval  42091  hvmapffval  42618  hvmapfval  42619  hdmap1fval  42656  hdmapffval  42686  hdmapfval  42687  hgmapfval  42746  wessf1ornlem  46004