Theorem riotaeqbidv 7358

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  ℩crio 7354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868  df-iota 6479  df-riota 7355

This theorem is referenced by:  dfoi  9461  oieq1  9462  oieq2  9463  ordtypecbv  9467  ordtypelem3  9470  zorn2lem1  10455  zorn2g  10462  cidfval  17710  cidval  17711  cidpropd  17744  lubfval  18382  glbfval  18395  grpinvfval  19022  grpinvfvalALT  19023  pj1fval  19736  mpfrcl  22140  evlsval  22141  q1pval  26217  ig1pval  26238  cutsval  27875  mirval  28830  midf  28951  ismidb  28953  lmif  28960  islmib  28962  gidval  30717  grpoinvfval  30727  pjhfval  31601  cvmliftlem5  35644  cvmliftlem15  35653  weiunlem  36828  trlfset  40789  dicffval  41803  dicfval  41804  dihffval  41859  dihfval  41860  hvmapffval  42387  hvmapfval  42388  hdmap1fval  42425  hdmapffval  42455  hdmapfval  42456  hgmapfval  42515  wessf1ornlem  45768