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	|- ( F/_ x A -> ( E. x x = A <-> E. y y = A ) )

Proof

Step	Hyp	Ref	Expression
1		nfnfc1	|- F/ x F/_ x A
2		nfv	|- F/ y F/_ x A
3		nfvd	|- ( F/_ x A -> F/ y -. x = A )
4		nfcvd	|- ( F/_ x A -> F/_ x y )
5		id	|- ( F/_ x A -> F/_ x A )
6	4 5	nfeqd	|- ( F/_ x A -> F/ x y = A )
7	6	nfnd	|- ( F/_ x A -> F/ x -. y = A )
8		eqeq1	|- ( x = y -> ( x = A <-> y = A ) )
9	8	notbid	|- ( x = y -> ( -. x = A <-> -. y = A ) )
10	9	a1i	|- ( F/_ x A -> ( x = y -> ( -. x = A <-> -. y = A ) ) )
11	1 2 3 7 10	cbv2w	|- ( F/_ x A -> ( A. x -. x = A <-> A. y -. y = A ) )
12		alnex	|- ( A. x -. x = A <-> -. E. x x = A )
13		alnex	|- ( A. y -. y = A <-> -. E. y y = A )
14	11 12 13	3bitr3g	|- ( F/_ x A -> ( -. E. x x = A <-> -. E. y y = A ) )
15	14	con4bid	|- ( F/_ x A -> ( E. x x = A <-> E. y y = A ) )