Metamath Proof Explorer


Theorem ovanraleqv

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)

Ref Expression
Hypothesis ovanraleqv.1 โŠข ( ๐ต = ๐‘‹ โ†’ ( ๐œ‘ โ†” ๐œ“ ) )
Assertion ovanraleqv ( ๐ต = ๐‘‹ โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘‰ ( ๐œ‘ โˆง ( ๐ด ยท ๐ต ) = ๐ถ ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐‘‰ ( ๐œ“ โˆง ( ๐ด ยท ๐‘‹ ) = ๐ถ ) ) )

Proof

Step Hyp Ref Expression
1 ovanraleqv.1 โŠข ( ๐ต = ๐‘‹ โ†’ ( ๐œ‘ โ†” ๐œ“ ) )
2 oveq2 โŠข ( ๐ต = ๐‘‹ โ†’ ( ๐ด ยท ๐ต ) = ( ๐ด ยท ๐‘‹ ) )
3 2 eqeq1d โŠข ( ๐ต = ๐‘‹ โ†’ ( ( ๐ด ยท ๐ต ) = ๐ถ โ†” ( ๐ด ยท ๐‘‹ ) = ๐ถ ) )
4 1 3 anbi12d โŠข ( ๐ต = ๐‘‹ โ†’ ( ( ๐œ‘ โˆง ( ๐ด ยท ๐ต ) = ๐ถ ) โ†” ( ๐œ“ โˆง ( ๐ด ยท ๐‘‹ ) = ๐ถ ) ) )
5 4 ralbidv โŠข ( ๐ต = ๐‘‹ โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘‰ ( ๐œ‘ โˆง ( ๐ด ยท ๐ต ) = ๐ถ ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐‘‰ ( ๐œ“ โˆง ( ๐ด ยท ๐‘‹ ) = ๐ถ ) ) )