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 A B x x = A φ ψ A x | φ ψ

Proof

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