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

Theorem riotaeqbidv 7116
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 7115 . 2 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐴 𝜒))
3 riotaeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
43riotaeqdv 7114 . 2 (𝜑 → (𝑥𝐴 𝜒) = (𝑥𝐵 𝜒))
52, 4eqtrd 2856 1 (𝜑 → (𝑥𝐴 𝜓) = (𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1533  crio 7112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951  df-uni 4838  df-iota 6313  df-riota 7113
This theorem is referenced by:  dfoi  8974  oieq1  8975  oieq2  8976  ordtypecbv  8980  ordtypelem3  8983  zorn2lem1  9917  zorn2g  9924  cidfval  16946  cidval  16947  cidpropd  16979  lubfval  17587  glbfval  17600  grpinvfval  18141  grpinvfvalALT  18142  pj1fval  18819  mpfrcl  20297  evlsval  20298  q1pval  24746  ig1pval  24765  mirval  26440  midf  26561  ismidb  26563  lmif  26570  islmib  26572  gidval  28288  grpoinvfval  28298  pjhfval  29172  cvmliftlem5  32536  cvmliftlem15  32545  scutval  33265  trlfset  37295  dicffval  38309  dicfval  38310  dihffval  38365  dihfval  38366  hvmapffval  38893  hvmapfval  38894  hdmap1fval  38931  hdmapffval  38961  hdmapfval  38962  hgmapfval  39021  wessf1ornlem  41445
  Copyright terms: Public domain W3C validator