Metamath Proof Explorer


Theorem mpteq12dfOLD

Description: Obsolete version of mpteq12df as of 11-Nov-2024. (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 11-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mpteq12df.1 xφ
mpteq12df.2 φA=C
mpteq12df.3 φB=D
Assertion mpteq12dfOLD φxAB=xCD

Proof

Step Hyp Ref Expression
1 mpteq12df.1 xφ
2 mpteq12df.2 φA=C
3 mpteq12df.3 φB=D
4 nfv yφ
5 2 eleq2d φxAxC
6 3 eqeq2d φy=By=D
7 5 6 anbi12d φxAy=BxCy=D
8 1 4 7 opabbid φxy|xAy=B=xy|xCy=D
9 df-mpt xAB=xy|xAy=B
10 df-mpt xCD=xy|xCy=D
11 8 9 10 3eqtr4g φxAB=xCD