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 = A y = B φ ψ
Assertion copsex2gOLD A V B W x y A B = x y φ ψ

Proof

Step Hyp Ref Expression
1 copsex2g.1 x = A y = B φ ψ
2 elisset A V x x = A
3 elisset B W y y = B
4 exdistrv x y x = A y = B x x = A y y = B
5 nfe1 x x y A B = x y φ
6 nfv x ψ
7 5 6 nfbi x x y A B = x y φ ψ
8 nfe1 y y A B = x y φ
9 8 nfex y x y A B = x y φ
10 nfv y ψ
11 9 10 nfbi y x y A B = x y φ ψ
12 opeq12 x = A y = B x y = A B
13 copsexgw A B = x y φ x y A B = x y φ
14 13 eqcoms x y = A B φ x y A B = x y φ
15 12 14 syl x = A y = B φ x y A B = x y φ
16 15 1 bitr3d x = A y = B x y A B = x y φ ψ
17 11 16 exlimi y x = A y = B x y A B = x y φ ψ
18 7 17 exlimi x y x = A y = B x y A B = x y φ ψ
19 4 18 sylbir x x = A y y = B x y A B = x y φ ψ
20 2 3 19 syl2an A V B W x y A B = x y φ ψ