Theorem riotaeqbidv 7350

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875  df-iota 6467  df-riota 7347

This theorem is referenced by:  dfoi  9471  oieq1  9472  oieq2  9473  ordtypecbv  9477  ordtypelem3  9480  zorn2lem1  10456  zorn2g  10463  cidfval  17644  cidval  17645  cidpropd  17678  lubfval  18316  glbfval  18329  grpinvfval  18917  grpinvfvalALT  18918  pj1fval  19631  mpfrcl  21999  evlsval  22000  q1pval  26067  ig1pval  26088  scutval  27719  mirval  28589  midf  28710  ismidb  28712  lmif  28719  islmib  28721  gidval  30448  grpoinvfval  30458  pjhfval  31332  cvmliftlem5  35283  cvmliftlem15  35292  weiunlem2  36458  trlfset  40161  dicffval  41175  dicfval  41176  dihffval  41231  dihfval  41232  hvmapffval  41759  hvmapfval  41760  hdmap1fval  41797  hdmapffval  41827  hdmapfval  41828  hgmapfval  41887  wessf1ornlem  45186