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

Theorem ovanraleqv 7382
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 7366 . . . 4 (๐ต = ๐‘‹ โ†’ (๐ด ยท ๐ต) = (๐ด ยท ๐‘‹))
32eqeq1d 2739 . . 3 (๐ต = ๐‘‹ โ†’ ((๐ด ยท ๐ต) = ๐ถ โ†” (๐ด ยท ๐‘‹) = ๐ถ))
41, 3anbi12d 632 . 2 (๐ต = ๐‘‹ โ†’ ((๐œ‘ โˆง (๐ด ยท ๐ต) = ๐ถ) โ†” (๐œ“ โˆง (๐ด ยท ๐‘‹) = ๐ถ)))
54ralbidv 3175 1 (๐ต = ๐‘‹ โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘‰ (๐œ‘ โˆง (๐ด ยท ๐ต) = ๐ถ) โ†” โˆ€๐‘ฅ โˆˆ ๐‘‰ (๐œ“ โˆง (๐ด ยท ๐‘‹) = ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542  โˆ€wral 3065  (class class class)co 7358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  mgmidmo  18516  ismgmid  18521  ismgmid2  18524  mgmidsssn0  18528  gsumvalx  18532  gsumress  18538  sgrpidmnd  18562  ismndd  18579  mnd1  18598  gsumvallem2  18645  mhmmnd  18870  rngurd  32068  signsw0g  33171  signswmnd  33172  exidu1  36318  cmpidelt  36321  exidres  36340  exidresid  36341  isrngod  36360  rngoideu  36365  zlidlring  46233  2zrngamnd  46246
  Copyright terms: Public domain W3C validator