Metamath Proof Explorer


Theorem spcimgfi1OLD

Description: Obsolete version of spcimgfi1 as of 27-Jul-2025. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses spcimgfi1.1 x ψ
spcimgfi1.2 _ x A
Assertion spcimgfi1OLD x x = A φ ψ A B x φ ψ

Proof

Step Hyp Ref Expression
1 spcimgfi1.1 x ψ
2 spcimgfi1.2 _ x A
3 elex A B A V
4 2 issetf A V x x = A
5 exim x x = A φ ψ x x = A x φ ψ
6 4 5 biimtrid x x = A φ ψ A V x φ ψ
7 1 19.36 x φ ψ x φ ψ
8 6 7 imbitrdi x x = A φ ψ A V x φ ψ
9 3 8 syl5 x x = A φ ψ A B x φ ψ