Theorem bj-vn0ALT

Description: Alternate proof of vn0 which does not use eqabbw (and is shorter than vn0 when eqabbw is inlined). (Contributed by BJ, 12-Jul-2026) Using the same dummy variable for y and z slightly reduces the proof size. (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-vn0ALT	|- _V =/= (/)

Proof

Step	Hyp	Ref	Expression
1		fal	|- -. F.
2		dfv2	|- _V = { y | T. }
3		dfnul4	|- (/) = { z | F. }
4	2 3	eqeq12i	|- ( _V = (/) <-> { y | T. } = { z | F. } )
5		dfcleq	|- ( { y | T. } = { z | F. } <-> A. x ( x e. { y | T. } <-> x e. { z | F. } ) )
6		df-clab	|- ( x e. { y | T. } <-> [ x / y ] T. )
7		sbv	|- ( [ x / y ] T. <-> T. )
8	6 7	bitri	|- ( x e. { y | T. } <-> T. )
9		df-clab	|- ( x e. { z | F. } <-> [ x / z ] F. )
10		sbv	|- ( [ x / z ] F. <-> F. )
11	9 10	bitri	|- ( x e. { z | F. } <-> F. )
12	8 11	bibi12i	|- ( ( x e. { y | T. } <-> x e. { z | F. } ) <-> ( T. <-> F. ) )
13		trubifal	|- ( ( T. <-> F. ) <-> F. )
14	12 13	sylbb	|- ( ( x e. { y | T. } <-> x e. { z | F. } ) -> F. )
15	14	spsv	|- ( A. x ( x e. { y | T. } <-> x e. { z | F. } ) -> F. )
16	5 15	sylbi	|- ( { y | T. } = { z | F. } -> F. )
17	4 16	sylbi	|- ( _V = (/) -> F. )
18	1 17	mto	|- -. _V = (/)
19	18	neir	|- _V =/= (/)