# 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 ( ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) ∧ 𝐴𝑉 ) → 𝜓 )

### Proof

Step Hyp Ref Expression
1 elisset ( 𝐴𝑉 → ∃ 𝑧 𝑧 = 𝐴 )
2 nfnfc1 𝑥 𝑥 𝐴
3 nfcvd ( 𝑥 𝐴 𝑥 𝑧 )
4 id ( 𝑥 𝐴 𝑥 𝐴 )
5 3 4 nfeqd ( 𝑥 𝐴 → Ⅎ 𝑥 𝑧 = 𝐴 )
6 eqeq1 ( 𝑧 = 𝑥 → ( 𝑧 = 𝐴𝑥 = 𝐴 ) )
7 6 a1i ( 𝑥 𝐴 → ( 𝑧 = 𝑥 → ( 𝑧 = 𝐴𝑥 = 𝐴 ) ) )
8 2 5 7 cbvexd ( 𝑥 𝐴 → ( ∃ 𝑧 𝑧 = 𝐴 ↔ ∃ 𝑥 𝑥 = 𝐴 ) )
9 1 8 syl5ib ( 𝑥 𝐴 → ( 𝐴𝑉 → ∃ 𝑥 𝑥 = 𝐴 ) )
10 9 ad2antrr ( ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) ) → ( 𝐴𝑉 → ∃ 𝑥 𝑥 = 𝐴 ) )
11 10 3impia ( ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) ∧ 𝐴𝑉 ) → ∃ 𝑥 𝑥 = 𝐴 )
12 biimp ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) )
13 12 imim2i ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) )
14 13 com23 ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( 𝜑 → ( 𝑥 = 𝐴𝜓 ) ) )
15 14 imp ( ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ 𝜑 ) → ( 𝑥 = 𝐴𝜓 ) )
16 15 alanimi ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝐴𝜓 ) )
17 19.23t ( Ⅎ 𝑥 𝜓 → ( ∀ 𝑥 ( 𝑥 = 𝐴𝜓 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴𝜓 ) ) )
18 17 adantl ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴𝜓 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴𝜓 ) ) )
19 16 18 syl5ib ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) → ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) → ( ∃ 𝑥 𝑥 = 𝐴𝜓 ) ) )
20 19 imp ( ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) ) → ( ∃ 𝑥 𝑥 = 𝐴𝜓 ) )
21 20 3adant3 ( ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) ∧ 𝐴𝑉 ) → ( ∃ 𝑥 𝑥 = 𝐴𝜓 ) )
22 11 21 mpd ( ( ( 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) ∧ 𝐴𝑉 ) → 𝜓 )