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