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	$$⊢B=X\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ovanraleqv	$$⊢B=X\to \left(\forall x\in V\left(\phi \wedge A\underset{\dot{}}{·}B=C\right)\leftrightarrow \forall x\in V\left(\psi \wedge A\underset{\dot{}}{·}X=C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovanraleqv.1	$$⊢B=X\to \left(\phi \leftrightarrow \psi \right)$$
2		oveq2	$$⊢B=X\to A\underset{\dot{}}{·}B=A\underset{\dot{}}{·}X$$
3	2	eqeq1d	$$⊢B=X\to \left(A\underset{\dot{}}{·}B=C\leftrightarrow A\underset{\dot{}}{·}X=C\right)$$
4	1 3	anbi12d	$$⊢B=X\to \left(\left(\phi \wedge A\underset{\dot{}}{·}B=C\right)\leftrightarrow \left(\psi \wedge A\underset{\dot{}}{·}X=C\right)\right)$$
5	4	ralbidv	$$⊢B=X\to \left(\forall x\in V\left(\phi \wedge A\underset{\dot{}}{·}B=C\right)\leftrightarrow \forall x\in V\left(\psi \wedge A\underset{\dot{}}{·}X=C\right)\right)$$