Theorem riotaeqbidv 7111

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

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

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 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-uni 4799  df-iota 6294  df-riota 7108

This theorem is referenced by:  dfoi  9008  oieq1  9009  oieq2  9010  ordtypecbv  9014  ordtypelem3  9017  zorn2lem1  9956  zorn2g  9963  cidfval  17005  cidval  17006  cidpropd  17038  lubfval  17654  glbfval  17667  grpinvfval  18209  grpinvfvalALT  18210  pj1fval  18887  mpfrcl  20848  evlsval  20849  q1pval  24853  ig1pval  24872  mirval  26548  midf  26669  ismidb  26671  lmif  26678  islmib  26680  gidval  28394  grpoinvfval  28404  pjhfval  29278  cvmliftlem5  32767  cvmliftlem15  32776  scutval  33557  trlfset  37736  dicffval  38750  dicfval  38751  dihffval  38806  dihfval  38807  hvmapffval  39334  hvmapfval  39335  hdmap1fval  39372  hdmapffval  39402  hdmapfval  39403  hgmapfval  39462  wessf1ornlem  42181