Metamath Proof Explorer


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 _ x A x x = A y y = A

Proof

Step Hyp Ref Expression
1 nfnfc1 x _ x A
2 nfv y _ x A
3 nfvd _ x A y ¬ x = A
4 nfcvd _ x A _ x y
5 id _ x A _ x A
6 4 5 nfeqd _ x A x y = A
7 6 nfnd _ x A x ¬ y = A
8 eqeq1 x = y x = A y = A
9 8 notbid x = y ¬ x = A ¬ y = A
10 9 a1i _ x A x = y ¬ x = A ¬ y = A
11 1 2 3 7 10 cbv2w _ x A x ¬ x = A y ¬ y = A
12 alnex x ¬ x = A ¬ x x = A
13 alnex y ¬ y = A ¬ y y = A
14 11 12 13 3bitr3g _ x A ¬ x x = A ¬ y y = A
15 14 con4bid _ x A x x = A y y = A