Metamath Proof Explorer


Theorem rexab2OLD

Description: Obsolete version of rexab2 as of 1-Dec-2023. (Contributed by Mario Carneiro, 3-Sep-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ralab2.1 x=yψχ
Assertion rexab2OLD xy|φψyφχ

Proof

Step Hyp Ref Expression
1 ralab2.1 x=yψχ
2 df-rex xy|φψxxy|φψ
3 nfsab1 yxy|φ
4 nfv yψ
5 3 4 nfan yxy|φψ
6 nfv xφχ
7 eleq1w x=yxy|φyy|φ
8 abid yy|φφ
9 7 8 bitrdi x=yxy|φφ
10 9 1 anbi12d x=yxy|φψφχ
11 5 6 10 cbvexv1 xxy|φψyφχ
12 2 11 bitri xy|φψyφχ