Metamath Proof Explorer


Theorem copsex2gOLD

Description: Obsolete version of copsex2g as of 1-Sep-2024. (Contributed by NM, 28-May-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis copsex2g.1 x=Ay=Bφψ
Assertion copsex2gOLD AVBWxyAB=xyφψ

Proof

Step Hyp Ref Expression
1 copsex2g.1 x=Ay=Bφψ
2 elisset AVxx=A
3 elisset BWyy=B
4 exdistrv xyx=Ay=Bxx=Ayy=B
5 nfe1 xxyAB=xyφ
6 nfv xψ
7 5 6 nfbi xxyAB=xyφψ
8 nfe1 yyAB=xyφ
9 8 nfex yxyAB=xyφ
10 nfv yψ
11 9 10 nfbi yxyAB=xyφψ
12 opeq12 x=Ay=Bxy=AB
13 copsexgw AB=xyφxyAB=xyφ
14 13 eqcoms xy=ABφxyAB=xyφ
15 12 14 syl x=Ay=BφxyAB=xyφ
16 15 1 bitr3d x=Ay=BxyAB=xyφψ
17 11 16 exlimi yx=Ay=BxyAB=xyφψ
18 7 17 exlimi xyx=Ay=BxyAB=xyφψ
19 4 18 sylbir xx=Ayy=BxyAB=xyφψ
20 2 3 19 syl2an AVBWxyAB=xyφψ