Theorem riotaeqbidv 6868

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1658  ℩crio 6864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rex 3122  df-uni 4658  df-iota 6085  df-riota 6865

This theorem is referenced by:  dfoi  8684  oieq1  8685  oieq2  8686  ordtypecbv  8690  ordtypelem3  8693  zorn2lem1  9632  zorn2g  9639  cidfval  16688  cidval  16689  cidpropd  16721  lubfval  17330  glbfval  17343  grpinvfval  17813  pj1fval  18457  mpfrcl  19877  evlsval  19878  q1pval  24311  ig1pval  24330  mirval  25966  midf  26084  ismidb  26086  lmif  26093  islmib  26095  gidval  27921  grpoinvfval  27931  pjhfval  28809  cvmliftlem5  31816  cvmliftlem15  31825  scutval  32449  trlfset  36234  dicffval  37248  dicfval  37249  dihffval  37304  dihfval  37305  hvmapffval  37832  hvmapfval  37833  hdmap1fval  37870  hdmapffval  37900  hdmapfval  37901  hgmapfval  37960  wessf1ornlem  40178