# Metamath Proof Explorer

## Theorem vtoclgftOLD

Description: Obsolete version of vtoclgft as of 6-Oct-2023. (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion vtoclgftOLD
`|- ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ps )`

### Proof

Step Hyp Ref Expression
1 elisset
` |-  ( A e. V -> E. z z = A )`
2 nfnfc1
` |-  F/ x F/_ x A`
3 nfcvd
` |-  ( F/_ x A -> F/_ x z )`
4 id
` |-  ( F/_ x A -> F/_ x A )`
5 3 4 nfeqd
` |-  ( F/_ x A -> F/ x z = A )`
6 eqeq1
` |-  ( z = x -> ( z = A <-> x = A ) )`
7 6 a1i
` |-  ( F/_ x A -> ( z = x -> ( z = A <-> x = A ) ) )`
8 2 5 7 cbvexd
` |-  ( F/_ x A -> ( E. z z = A <-> E. x x = A ) )`
9 1 8 syl5ib
` |-  ( F/_ x A -> ( A e. V -> E. x x = A ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( A e. V -> E. x x = A ) )`
11 10 3impia
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> E. x x = A )`
12 biimp
` |-  ( ( ph <-> ps ) -> ( ph -> ps ) )`
13 12 imim2i
` |-  ( ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ph -> ps ) ) )`
14 13 com23
` |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ph -> ( x = A -> ps ) ) )`
15 14 imp
` |-  ( ( ( x = A -> ( ph <-> ps ) ) /\ ph ) -> ( x = A -> ps ) )`
16 15 alanimi
` |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> A. x ( x = A -> ps ) )`
17 19.23t
` |-  ( F/ x ps -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )`
` |-  ( ( F/_ x A /\ F/ x ps ) -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )`
` |-  ( ( F/_ x A /\ F/ x ps ) -> ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> ( E. x x = A -> ps ) ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( E. x x = A -> ps ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ( E. x x = A -> ps ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ps )`