Theorem riotaeqbidv 7380

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-iota 6494  df-riota 7377

This theorem is used by:  dfoi  9505  oieq1  9506  oieq2  9507  ordtypecbv  9511  ordtypelem3  9514  zorn2lem1  10574  zorn2g  10581  cidfval  17850  cidval  17851  cidpropd  17884  lubfval  18522  glbfval  18535  grpinvfval  19189  grpinvfvalALT  19190  pj1fval  19908  mpfrcl  22394  evlsval  22395  q1pval  26473  ig1pval  26494  cutsval  28166  mirval  29127  midf  29281  ismidb  29283  lmif  29290  islmib  29292  angmgmval  29394  gidval  31114  grpoinvfval  31124  pjhfval  31998  cvmliftlem5  36054  cvmliftlem15  36063  weiunlem  37251  trlfset  41218  dicffval  42232  dicfval  42233  dihffval  42288  dihfval  42289  hvmapffval  42816  hvmapfval  42817  hdmap1fval  42854  hdmapffval  42884  hdmapfval  42885  hgmapfval  42944  wessf1ornlem  46200