Theorem riotaeqbidv 7370

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ℩crio 7366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-iota 6494  df-riota 7367

This theorem is referenced by:  dfoi  9508  oieq1  9509  oieq2  9510  ordtypecbv  9514  ordtypelem3  9517  zorn2lem1  10493  zorn2g  10500  cidfval  17624  cidval  17625  cidpropd  17658  lubfval  18307  glbfval  18320  grpinvfval  18899  grpinvfvalALT  18900  pj1fval  19603  mpfrcl  21867  evlsval  21868  q1pval  25906  ig1pval  25925  scutval  27538  mirval  28173  midf  28294  ismidb  28296  lmif  28303  islmib  28305  gidval  30032  grpoinvfval  30042  pjhfval  30916  cvmliftlem5  34578  cvmliftlem15  34587  trlfset  39334  dicffval  40348  dicfval  40349  dihffval  40404  dihfval  40405  hvmapffval  40932  hvmapfval  40933  hdmap1fval  40970  hdmapffval  41000  hdmapfval  41001  hgmapfval  41060  wessf1ornlem  44182