Theorem riotaeqbidv 7320

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ℩crio 7316

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865  df-iota 6449  df-riota 7317

This theorem is referenced by:  dfoi  9420  oieq1  9421  oieq2  9422  ordtypecbv  9426  ordtypelem3  9429  zorn2lem1  10410  zorn2g  10417  cidfval  17603  cidval  17604  cidpropd  17637  lubfval  18275  glbfval  18288  grpinvfval  18912  grpinvfvalALT  18913  pj1fval  19627  mpfrcl  22044  evlsval  22045  q1pval  26120  ig1pval  26141  cutsval  27780  mirval  28731  midf  28852  ismidb  28854  lmif  28861  islmib  28863  gidval  30591  grpoinvfval  30601  pjhfval  31475  cvmliftlem5  35485  cvmliftlem15  35494  weiunlem  36659  trlfset  40488  dicffval  41502  dicfval  41503  dihffval  41558  dihfval  41559  hvmapffval  42086  hvmapfval  42087  hdmap1fval  42124  hdmapffval  42154  hdmapfval  42155  hgmapfval  42214  wessf1ornlem  45496