Theorem riotaeqbidv 7368

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ℩crio 7364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-uni 4867  df-iota 6483  df-riota 7365

This theorem is used by:  dfoi  9483  oieq1  9484  oieq2  9485  ordtypecbv  9489  ordtypelem3  9492  zorn2lem1  10545  zorn2g  10552  cidfval  17811  cidval  17812  cidpropd  17845  lubfval  18483  glbfval  18496  grpinvfval  19150  grpinvfvalALT  19151  pj1fval  19869  mpfrcl  22355  evlsval  22356  q1pval  26434  ig1pval  26455  cutsval  28099  mirval  29060  midf  29214  ismidb  29216  lmif  29223  islmib  29225  angmgmval  29327  gidval  31047  grpoinvfval  31057  pjhfval  31931  cvmliftlem5  35975  cvmliftlem15  35984  weiunlem  37173  trlfset  41137  dicffval  42151  dicfval  42152  dihffval  42207  dihfval  42208  hvmapffval  42735  hvmapfval  42736  hdmap1fval  42773  hdmapffval  42803  hdmapfval  42804  hgmapfval  42863  wessf1ornlem  46121