Theorem riotaeqbidv 7119

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ℩crio 7115

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841  df-iota 6316  df-riota 7116

This theorem is referenced by:  dfoi  8977  oieq1  8978  oieq2  8979  ordtypecbv  8983  ordtypelem3  8986  zorn2lem1  9920  zorn2g  9927  cidfval  16949  cidval  16950  cidpropd  16982  lubfval  17590  glbfval  17603  grpinvfval  18144  grpinvfvalALT  18145  pj1fval  18822  mpfrcl  20300  evlsval  20301  q1pval  24749  ig1pval  24768  mirval  26443  midf  26564  ismidb  26566  lmif  26573  islmib  26575  gidval  28291  grpoinvfval  28301  pjhfval  29175  cvmliftlem5  32538  cvmliftlem15  32547  scutval  33267  trlfset  37298  dicffval  38312  dicfval  38313  dihffval  38368  dihfval  38369  hvmapffval  38896  hvmapfval  38897  hdmap1fval  38934  hdmapffval  38964  hdmapfval  38965  hgmapfval  39024  wessf1ornlem  41452