Theorem riotaeqbidv 7370

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889  df-iota 6489  df-riota 7367

This theorem is referenced by:  dfoi  9530  oieq1  9531  oieq2  9532  ordtypecbv  9536  ordtypelem3  9539  zorn2lem1  10515  zorn2g  10522  cidfval  17693  cidval  17694  cidpropd  17727  lubfval  18365  glbfval  18378  grpinvfval  18966  grpinvfvalALT  18967  pj1fval  19680  mpfrcl  22048  evlsval  22049  q1pval  26117  ig1pval  26138  scutval  27769  mirval  28639  midf  28760  ismidb  28762  lmif  28769  islmib  28771  gidval  30498  grpoinvfval  30508  pjhfval  31382  cvmliftlem5  35316  cvmliftlem15  35325  weiunlem2  36486  trlfset  40184  dicffval  41198  dicfval  41199  dihffval  41254  dihfval  41255  hvmapffval  41782  hvmapfval  41783  hdmap1fval  41820  hdmapffval  41850  hdmapfval  41851  hgmapfval  41910  wessf1ornlem  45176