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

Theorem ovanraleqv 7455
Description: Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
Hypothesis
Ref Expression
ovanraleqv.1 (𝐵 = 𝑋 → (𝜑𝜓))
Assertion
Ref Expression
ovanraleqv (𝐵 = 𝑋 → (∀𝑥𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))
Distinct variable groups:   𝑥,𝐵   𝑥,𝑋
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝐴(𝑥)   𝐶(𝑥)   · (𝑥)   𝑉(𝑥)

Proof of Theorem ovanraleqv
StepHypRef Expression
1 ovanraleqv.1 . . 3 (𝐵 = 𝑋 → (𝜑𝜓))
2 oveq2 7439 . . . 4 (𝐵 = 𝑋 → (𝐴 · 𝐵) = (𝐴 · 𝑋))
32eqeq1d 2737 . . 3 (𝐵 = 𝑋 → ((𝐴 · 𝐵) = 𝐶 ↔ (𝐴 · 𝑋) = 𝐶))
41, 3anbi12d 632 . 2 (𝐵 = 𝑋 → ((𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))
54ralbidv 3176 1 (𝐵 = 𝑋 → (∀𝑥𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wral 3059  (class class class)co 7431
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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434
This theorem is referenced by:  mgmidmo  18686  ismgmid  18691  ismgmid2  18694  mgmidsssn0  18698  gsumvalx  18702  gsumress  18708  sgrpidmnd  18765  ismndd  18782  mnd1  18805  gsumvallem2  18860  mhmmnd  19095  ringurd  20203  opprring  20364  pzriprnglem7  21516  pzriprnglem13  21522  signsw0g  34550  signswmnd  34551  exidu1  37843  cmpidelt  37846  exidres  37865  exidresid  37866  isrngod  37885  rngoideu  37890  zlidlring  48078  2zrngamnd  48091
  Copyright terms: Public domain W3C validator