Theorem riotaeqbidv 7368

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ℩crio 7364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-iota 6496  df-riota 7365

This theorem is referenced by:  dfoi  9506  oieq1  9507  oieq2  9508  ordtypecbv  9512  ordtypelem3  9515  zorn2lem1  10491  zorn2g  10498  cidfval  17620  cidval  17621  cidpropd  17654  lubfval  18303  glbfval  18316  grpinvfval  18863  grpinvfvalALT  18864  pj1fval  19562  mpfrcl  21648  evlsval  21649  q1pval  25671  ig1pval  25690  scutval  27301  mirval  27906  midf  28027  ismidb  28029  lmif  28036  islmib  28038  gidval  29765  grpoinvfval  29775  pjhfval  30649  cvmliftlem5  34280  cvmliftlem15  34289  trlfset  39031  dicffval  40045  dicfval  40046  dihffval  40101  dihfval  40102  hvmapffval  40629  hvmapfval  40630  hdmap1fval  40667  hdmapffval  40697  hdmapfval  40698  hgmapfval  40757  wessf1ornlem  43882