Metamath Proof Explorer


Theorem rexcomOLD

Description: Obsolete version of rexcom as of 8-Dec-2024. (Contributed by NM, 19-Nov-1995) (Revised by Mario Carneiro, 14-Oct-2016) (Proof shortened by BJ, 26-Aug-2023) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion rexcomOLD xAyBφyBxAφ

Proof

Step Hyp Ref Expression
1 df-rex yBφyyBφ
2 1 rexbii xAyBφxAyyBφ
3 rexcom4 xAyyBφyxAyBφ
4 r19.42v xAyBφyBxAφ
5 4 exbii yxAyBφyyBxAφ
6 df-rex yBxAφyyBxAφ
7 5 6 bitr4i yxAyBφyBxAφ
8 2 3 7 3bitri xAyBφyBxAφ