Metamath Proof Explorer


Theorem elabgtOLD

Description: Obsolete version of elabgt as of 12-Oct-2024. (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elabgtOLD ABxx=AφψAx|φψ

Proof

Step Hyp Ref Expression
1 nfcv _xA
2 nfab1 _xx|φ
3 2 nfel2 xAx|φ
4 nfv xψ
5 3 4 nfbi xAx|φψ
6 pm5.5 x=Ax=AAx|φψAx|φψ
7 1 5 6 spcgf ABxx=AAx|φψAx|φψ
8 abid xx|φφ
9 eleq1 x=Axx|φAx|φ
10 8 9 bitr3id x=AφAx|φ
11 10 bibi1d x=AφψAx|φψ
12 11 biimpd x=AφψAx|φψ
13 12 a2i x=Aφψx=AAx|φψ
14 13 alimi xx=Aφψxx=AAx|φψ
15 7 14 impel ABxx=AφψAx|φψ