Metamath Proof Explorer


Theorem ralab2OLD

Description: Obsolete version of ralab2 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 ralab2OLD xy|φψyφχ

Proof

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