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 Gino Giotto, 6-Oct-2023)

	Ref	Expression
Assertion	vtoclgft	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\wedge A\in V\right)\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		issetft	$$⊢\underset{\_}{Ⅎ}xA\to \left(A\in \mathrm{V}\leftrightarrow \exists xx=A\right)$$
3	1 2	imbitrid	$$⊢\underset{\_}{Ⅎ}xA\to \left(A\in V\to \exists xx=A\right)$$
4	3	ad2antrr	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\right)\to \left(A\in V\to \exists xx=A\right)$$
5	4	3impia	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\wedge A\in V\right)\to \exists xx=A$$
6		biimp	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\phi \to \psi \right)$$
7	6	imim2i	$$⊢\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(x=A\to \left(\phi \to \psi \right)\right)$$
8	7	com23	$$⊢\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\to \left(\phi \to \left(x=A\to \psi \right)\right)$$
9	8	imp	$$⊢\left(\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \phi \right)\to \left(x=A\to \psi \right)$$
10	9	alanimi	$$⊢\left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\to \forall x\left(x=A\to \psi \right)$$
11		19.23t	$$⊢Ⅎx\psi \to \left(\forall x\left(x=A\to \psi \right)\leftrightarrow \left(\exists xx=A\to \psi \right)\right)$$
12	11	adantl	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\to \left(\forall x\left(x=A\to \psi \right)\leftrightarrow \left(\exists xx=A\to \psi \right)\right)$$
13	10 12	imbitrid	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\to \left(\left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\to \left(\exists xx=A\to \psi \right)\right)$$
14	13	imp	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\right)\to \left(\exists xx=A\to \psi \right)$$
15	14	3adant3	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\wedge A\in V\right)\to \left(\exists xx=A\to \psi \right)$$
16	5 15	mpd	$$⊢\left(\left(\underset{\_}{Ⅎ}xA\wedge Ⅎx\psi \right)\wedge \left(\forall x\left(x=A\to \left(\phi \leftrightarrow \psi \right)\right)\wedge \forall x\phi \right)\wedge A\in V\right)\to \psi$$