Theorem imbrov2fvoveq

Description: Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022)

	Ref	Expression
Hypothesis	imbrov2fvoveq.1	$$⊢X=Y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	imbrov2fvoveq	$$⊢X=Y\to \left(\left(\phi \to F\left(G\left(X\right)\underset{\dot{}}{·}O\right)RA\right)\leftrightarrow \left(\psi \to F\left(G\left(Y\right)\underset{\dot{}}{·}O\right)RA\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		imbrov2fvoveq.1	$$⊢X=Y\to \left(\phi \leftrightarrow \psi \right)$$
2		fveq2	$$⊢X=Y\to G\left(X\right)=G\left(Y\right)$$
3	2	fvoveq1d	$$⊢X=Y\to F\left(G\left(X\right)\underset{\dot{}}{·}O\right)=F\left(G\left(Y\right)\underset{\dot{}}{·}O\right)$$
4	3	breq1d	$$⊢X=Y\to \left(F\left(G\left(X\right)\underset{\dot{}}{·}O\right)RA\leftrightarrow F\left(G\left(Y\right)\underset{\dot{}}{·}O\right)RA\right)$$
5	1 4	imbi12d	$$⊢X=Y\to \left(\left(\phi \to F\left(G\left(X\right)\underset{\dot{}}{·}O\right)RA\right)\leftrightarrow \left(\psi \to F\left(G\left(Y\right)\underset{\dot{}}{·}O\right)RA\right)\right)$$