Theorem riotaeqbidv 7309

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ℩crio 7305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859  df-iota 6438  df-riota 7306

This theorem is referenced by:  dfoi  9403  oieq1  9404  oieq2  9405  ordtypecbv  9409  ordtypelem3  9412  zorn2lem1  10390  zorn2g  10397  cidfval  17582  cidval  17583  cidpropd  17616  lubfval  18254  glbfval  18267  grpinvfval  18857  grpinvfvalALT  18858  pj1fval  19573  mpfrcl  21990  evlsval  21991  q1pval  26058  ig1pval  26079  scutval  27712  mirval  28604  midf  28725  ismidb  28727  lmif  28734  islmib  28736  gidval  30460  grpoinvfval  30470  pjhfval  31344  cvmliftlem5  35282  cvmliftlem15  35291  weiunlem2  36457  trlfset  40159  dicffval  41173  dicfval  41174  dihffval  41229  dihfval  41230  hvmapffval  41757  hvmapfval  41758  hdmap1fval  41795  hdmapffval  41825  hdmapfval  41826  hgmapfval  41885  wessf1ornlem  45183