Metamath Proof Explorer


Theorem spcimgfi1

Description: A closed version of spcimgf . (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by Wolf Lammen, 27-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 spcimgfi1.1 x ψ
2 spcimgfi1.2 _ x A
3 spcimgft _ x A x ψ x x = A φ ψ A B x φ ψ
4 3 ex _ x A x ψ x x = A φ ψ A B x φ ψ
5 2 1 4 mp2an x x = A φ ψ A B x φ ψ