Theorem riotaeqbidv 7324

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

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

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 3432  df-ss 3907  df-uni 4852  df-iota 6452  df-riota 7321

This theorem is referenced by:  dfoi  9423  oieq1  9424  oieq2  9425  ordtypecbv  9429  ordtypelem3  9432  zorn2lem1  10415  zorn2g  10422  cidfval  17639  cidval  17640  cidpropd  17673  lubfval  18311  glbfval  18324  grpinvfval  18951  grpinvfvalALT  18952  pj1fval  19666  mpfrcl  22079  evlsval  22080  q1pval  26136  ig1pval  26157  cutsval  27792  mirval  28743  midf  28864  ismidb  28866  lmif  28873  islmib  28875  gidval  30604  grpoinvfval  30614  pjhfval  31488  cvmliftlem5  35493  cvmliftlem15  35502  weiunlem  36667  trlfset  40628  dicffval  41642  dicfval  41643  dihffval  41698  dihfval  41699  hvmapffval  42226  hvmapfval  42227  hdmap1fval  42264  hdmapffval  42294  hdmapfval  42295  hgmapfval  42354  wessf1ornlem  45641