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

Theorem ovanraleqv 7435
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 7419 . . . 4 (๐ต = ๐‘‹ โ†’ (๐ด ยท ๐ต) = (๐ด ยท ๐‘‹))
32eqeq1d 2732 . . 3 (๐ต = ๐‘‹ โ†’ ((๐ด ยท ๐ต) = ๐ถ โ†” (๐ด ยท ๐‘‹) = ๐ถ))
41, 3anbi12d 629 . 2 (๐ต = ๐‘‹ โ†’ ((๐œ‘ โˆง (๐ด ยท ๐ต) = ๐ถ) โ†” (๐œ“ โˆง (๐ด ยท ๐‘‹) = ๐ถ)))
54ralbidv 3175 1 (๐ต = ๐‘‹ โ†’ (โˆ€๐‘ฅ โˆˆ ๐‘‰ (๐œ‘ โˆง (๐ด ยท ๐ต) = ๐ถ) โ†” โˆ€๐‘ฅ โˆˆ ๐‘‰ (๐œ“ โˆง (๐ด ยท ๐‘‹) = ๐ถ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1539  โˆ€wral 3059  (class class class)co 7411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414
This theorem is referenced by:  mgmidmo  18585  ismgmid  18590  ismgmid2  18593  mgmidsssn0  18597  gsumvalx  18601  gsumress  18607  sgrpidmnd  18664  ismndd  18681  mnd1  18701  gsumvallem2  18751  mhmmnd  18983  ringurd  20079  opprring  20238  pzriprnglem7  21256  pzriprnglem13  21262  signsw0g  33865  signswmnd  33866  exidu1  37027  cmpidelt  37030  exidres  37049  exidresid  37050  isrngod  37069  rngoideu  37074  zlidlring  46914  2zrngamnd  46927
  Copyright terms: Public domain W3C validator