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

Theorem ovanraleqv 7295
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 7279 . . . 4 (𝐵 = 𝑋 → (𝐴 · 𝐵) = (𝐴 · 𝑋))
32eqeq1d 2742 . . 3 (𝐵 = 𝑋 → ((𝐴 · 𝐵) = 𝐶 ↔ (𝐴 · 𝑋) = 𝐶))
41, 3anbi12d 631 . 2 (𝐵 = 𝑋 → ((𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))
54ralbidv 3123 1 (𝐵 = 𝑋 → (∀𝑥𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1542  wral 3066  (class class class)co 7271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-iota 6390  df-fv 6440  df-ov 7274
This theorem is referenced by:  mgmidmo  18342  ismgmid  18347  ismgmid2  18350  mgmidsssn0  18354  gsumvalx  18358  gsumress  18364  sgrpidmnd  18388  ismndd  18405  mnd1  18424  gsumvallem2  18470  mhmmnd  18695  rngurd  31478  signsw0g  32531  signswmnd  32532  exidu1  36010  cmpidelt  36013  exidres  36032  exidresid  36033  isrngod  36052  rngoideu  36057  zlidlring  45455  2zrngamnd  45468
  Copyright terms: Public domain W3C validator