Metamath Proof Explorer


Theorem vtoclgft

Description: Closed theorem form of vtoclgf . The reverse implication is proven in ceqsal1t . See ceqsalt for a version with x and A disjoint. (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) Avoid ax-13 . (Revised by GG, 6-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 biimp φ ψ φ ψ
2 1 imim2i x = A φ ψ x = A φ ψ
3 2 alimi x x = A φ ψ x x = A φ ψ
4 spcimgft _ x A x ψ x x = A φ ψ A V x φ ψ
5 3 4 sylan2 _ x A x ψ x x = A φ ψ A V x φ ψ
6 5 com23 _ x A x ψ x x = A φ ψ x φ A V ψ
7 6 impr _ x A x ψ x x = A φ ψ x φ A V ψ
8 7 3impia _ x A x ψ x x = A φ ψ x φ A V ψ