This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 ) )