Theorem issetft

Description: Closed theorem form of isset that does not require x and A to be distinct. Extracted from the proof of vtoclgft . (Contributed by Wolf Lammen, 9-Apr-2025)

	Ref	Expression
Assertion	issetft	⊢ ( Ⅎ 𝑥 𝐴 → ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑦 𝑦 = 𝐴 )
2		nfv	⊢ Ⅎ 𝑦 Ⅎ 𝑥 𝐴
3		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
4		nfcvd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 )
5		id	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝐴 )
6	4 5	nfeqd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 = 𝐴 )
7	6	nfnd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 ¬ 𝑦 = 𝐴 )
8		nfvd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑦 ¬ 𝑥 = 𝐴 )
9		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝐴 ↔ 𝑥 = 𝐴 ) )
10	9	notbid	⊢ ( 𝑦 = 𝑥 → ( ¬ 𝑦 = 𝐴 ↔ ¬ 𝑥 = 𝐴 ) )
11	10	a1i	⊢ ( Ⅎ 𝑥 𝐴 → ( 𝑦 = 𝑥 → ( ¬ 𝑦 = 𝐴 ↔ ¬ 𝑥 = 𝐴 ) ) )
12	2 3 7 8 11	cbv2w	⊢ ( Ⅎ 𝑥 𝐴 → ( ∀ 𝑦 ¬ 𝑦 = 𝐴 ↔ ∀ 𝑥 ¬ 𝑥 = 𝐴 ) )
13		alnex	⊢ ( ∀ 𝑦 ¬ 𝑦 = 𝐴 ↔ ¬ ∃ 𝑦 𝑦 = 𝐴 )
14		alnex	⊢ ( ∀ 𝑥 ¬ 𝑥 = 𝐴 ↔ ¬ ∃ 𝑥 𝑥 = 𝐴 )
15	12 13 14	3bitr3g	⊢ ( Ⅎ 𝑥 𝐴 → ( ¬ ∃ 𝑦 𝑦 = 𝐴 ↔ ¬ ∃ 𝑥 𝑥 = 𝐴 ) )
16	15	con4bid	⊢ ( Ⅎ 𝑥 𝐴 → ( ∃ 𝑦 𝑦 = 𝐴 ↔ ∃ 𝑥 𝑥 = 𝐴 ) )
17	1 16	bitrid	⊢ ( Ⅎ 𝑥 𝐴 → ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 ) )