Theorem mpteq2iaOLD

Description: Obsolete version of mpteq2ia as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	mpteq2ia.1	|- ( x e. A -> B = C )
Assertion	mpteq2iaOLD	|- ( x e. A |-> B ) = ( x e. A |-> C )

Proof

Step	Hyp	Ref	Expression
1		mpteq2ia.1	|- ( x e. A -> B = C )
2		eqid	|- A = A
3	2	ax-gen	|- A. x A = A
4	1	rgen	|- A. x e. A B = C
5		mpteq12f	|- ( ( A. x A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
6	3 4 5	mp2an	|- ( x e. A |-> B ) = ( x e. A |-> C )