oveqrspc2v

Description: Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014)

		Ref	Expression
	Hypothesis	oveqrspc2v.1	$⊢ (φ \land (x \in A \land y \in B)) \to x F y = x G y$
	Assertion	oveqrspc2v	$⊢ (φ \land (X \in A \land Y \in B)) \to X F Y = X G Y$

Step	Hyp	Ref	Expression
1		oveqrspc2v.1	$⊢ (φ \land (x \in A \land y \in B)) \to x F y = x G y$
2	1	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in B x F y = x G y$
3		oveq1	$⊢ x = X \to x F y = X F y$
4		oveq1	$⊢ x = X \to x G y = X G y$
5	3 4	eqeq12d	$⊢ x = X \to (x F y = x G y \leftrightarrow X F y = X G y)$
6		oveq2	$⊢ y = Y \to X F y = X F Y$
7		oveq2	$⊢ y = Y \to X G y = X G Y$
8	6 7	eqeq12d	$⊢ y = Y \to (X F y = X G y \leftrightarrow X F Y = X G Y)$
9	5 8	rspc2v	$⊢ (X \in A \land Y \in B) \to (\forall x \in A \forall y \in B x F y = x G y \to X F Y = X G Y)$
10	2 9	mpan9	$⊢ (φ \land (X \in A \land Y \in B)) \to X F Y = X G Y$

Metamath Proof Explorer