Theorem cbvexeqsetf

Description: The expression E. x x = A means " A is a set" even if A contains x as a bound variable. This lemma helps minimizing axiom or df-clab usage in some cases. Extracted from the proof of issetft . (Contributed by Wolf Lammen, 30-Jul-2025)

	Ref	Expression
Assertion	cbvexeqsetf	⊢ ( Ⅎ 𝑥 𝐴 → ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 ) )

Proof

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