Metamath Proof Explorer


Theorem spcimgft

Description: Closed theorem form of spcimgf . (Contributed by Wolf Lammen, 28-Jul-2025)

Ref Expression
Assertion spcimgft _ x A x ψ x x = A φ ψ A V x φ ψ

Proof

Step Hyp Ref Expression
1 elissetv A V y y = A
2 cbvexeqsetf _ x A x x = A y y = A
3 1 2 imbitrrid _ x A A V x x = A
4 pm2.04 x = A φ ψ φ x = A ψ
5 4 al2imi x x = A φ ψ x φ x x = A ψ
6 19.23t x ψ x x = A ψ x x = A ψ
7 6 biimpd x ψ x x = A ψ x x = A ψ
8 5 7 sylan9r x ψ x x = A φ ψ x φ x x = A ψ
9 8 com23 x ψ x x = A φ ψ x x = A x φ ψ
10 3 9 sylan9 _ x A x ψ x x = A φ ψ A V x φ ψ
11 10 anassrs _ x A x ψ x x = A φ ψ A V x φ ψ