MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  riotaeqbidv Structured version   Visualization version   GIF version

Theorem riotaeqbidv 7392
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
StepHypRef Expression
1 riotaeqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
21riotabidv 7391 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 7390 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2776 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1539  crio 7388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-uni 4907  df-iota 6513  df-riota 7389
This theorem is referenced by:  dfoi  9552  oieq1  9553  oieq2  9554  ordtypecbv  9558  ordtypelem3  9561  zorn2lem1  10537  zorn2g  10544  cidfval  17720  cidval  17721  cidpropd  17754  lubfval  18396  glbfval  18409  grpinvfval  18997  grpinvfvalALT  18998  pj1fval  19713  mpfrcl  22110  evlsval  22111  q1pval  26195  ig1pval  26216  scutval  27846  mirval  28664  midf  28785  ismidb  28787  lmif  28794  islmib  28796  gidval  30532  grpoinvfval  30542  pjhfval  31416  cvmliftlem5  35295  cvmliftlem15  35304  weiunlem2  36465  trlfset  40163  dicffval  41177  dicfval  41178  dihffval  41233  dihfval  41234  hvmapffval  41761  hvmapfval  41762  hdmap1fval  41799  hdmapffval  41829  hdmapfval  41830  hgmapfval  41889  wessf1ornlem  45195
  Copyright terms: Public domain W3C validator