Theorem riotaeqbidv 7385

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ℩crio 7381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966  df-uni 4913  df-iota 6505  df-riota 7382

This theorem is referenced by:  dfoi  9542  oieq1  9543  oieq2  9544  ordtypecbv  9548  ordtypelem3  9551  zorn2lem1  10527  zorn2g  10534  cidfval  17663  cidval  17664  cidpropd  17697  lubfval  18349  glbfval  18362  grpinvfval  18942  grpinvfvalALT  18943  pj1fval  19656  mpfrcl  22038  evlsval  22039  q1pval  26110  ig1pval  26130  scutval  27753  mirval  28479  midf  28600  ismidb  28602  lmif  28609  islmib  28611  gidval  30342  grpoinvfval  30352  pjhfval  31226  cvmliftlem5  34932  cvmliftlem15  34941  trlfset  39665  dicffval  40679  dicfval  40680  dihffval  40735  dihfval  40736  hvmapffval  41263  hvmapfval  41264  hdmap1fval  41301  hdmapffval  41331  hdmapfval  41332  hgmapfval  41391  wessf1ornlem  44588

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »