Theorem riotaeqbidv 7371

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ℩crio 7367

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-uni 4909  df-iota 6495  df-riota 7368

This theorem is referenced by:  dfoi  9510  oieq1  9511  oieq2  9512  ordtypecbv  9516  ordtypelem3  9519  zorn2lem1  10495  zorn2g  10502  cidfval  17625  cidval  17626  cidpropd  17659  lubfval  18308  glbfval  18321  grpinvfval  18900  grpinvfvalALT  18901  pj1fval  19604  mpfrcl  21868  evlsval  21869  q1pval  25907  ig1pval  25926  scutval  27539  mirval  28174  midf  28295  ismidb  28297  lmif  28304  islmib  28306  gidval  30033  grpoinvfval  30043  pjhfval  30917  cvmliftlem5  34579  cvmliftlem15  34588  trlfset  39335  dicffval  40349  dicfval  40350  dihffval  40405  dihfval  40406  hvmapffval  40933  hvmapfval  40934  hdmap1fval  40971  hdmapffval  41001  hdmapfval  41002  hgmapfval  41061  wessf1ornlem  44183