This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (φ \leftrightarrow ψ)$
	Assertion	imbrov2fvoveq	$⊢ X = Y \to ((φ \to F (G (X) \underset{˙}{\cdot} O) R A) \leftrightarrow (ψ \to F (G (Y) \underset{˙}{\cdot} O) R A))$

Proof

Step	Hyp	Ref	Expression
1		imbrov2fvoveq.1	$⊢ X = Y \to (φ \leftrightarrow ψ)$
2		fveq2	$⊢ X = Y \to G (X) = G (Y)$
3	2	fvoveq1d	$⊢ X = Y \to F (G (X) \underset{˙}{\cdot} O) = F (G (Y) \underset{˙}{\cdot} O)$
4	3	breq1d	$⊢ X = Y \to (F (G (X) \underset{˙}{\cdot} O) R A \leftrightarrow F (G (Y) \underset{˙}{\cdot} O) R A)$
5	1 4	imbi12d	$⊢ X = Y \to ((φ \to F (G (X) \underset{˙}{\cdot} O) R A) \leftrightarrow (ψ \to F (G (Y) \underset{˙}{\cdot} O) R A))$