Theorem riotaeqbidv 7096

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ℩crio 7092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-iota 6283  df-riota 7093

This theorem is referenced by:  dfoi  8959  oieq1  8960  oieq2  8961  ordtypecbv  8965  ordtypelem3  8968  zorn2lem1  9907  zorn2g  9914  cidfval  16939  cidval  16940  cidpropd  16972  lubfval  17580  glbfval  17593  grpinvfval  18134  grpinvfvalALT  18135  pj1fval  18812  mpfrcl  20757  evlsval  20758  q1pval  24754  ig1pval  24773  mirval  26449  midf  26570  ismidb  26572  lmif  26579  islmib  26581  gidval  28295  grpoinvfval  28305  pjhfval  29179  cvmliftlem5  32649  cvmliftlem15  32658  scutval  33378  trlfset  37456  dicffval  38470  dicfval  38471  dihffval  38526  dihfval  38527  hvmapffval  39054  hvmapfval  39055  hdmap1fval  39092  hdmapffval  39122  hdmapfval  39123  hgmapfval  39182  wessf1ornlem  41811