Theorem notzfausOLD

Description: Obsolete proof of notzfaus as of 18-Nov-2023. (Contributed by NM, 8-Feb-2006) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	notzfaus.1	|- A = { (/) }
	notzfaus.2	|- ( ph <-> -. x e. y )
Assertion	notzfausOLD	|- -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		notzfaus.1	|- A = { (/) }
2		notzfaus.2	|- ( ph <-> -. x e. y )
3		0ex	|- (/) e. _V
4	3	snnz	|- { (/) } =/= (/)
5	1 4	eqnetri	|- A =/= (/)
6		n0	|- ( A =/= (/) <-> E. x x e. A )
7	5 6	mpbi	|- E. x x e. A
8		biimt	|- ( x e. A -> ( x e. y <-> ( x e. A -> x e. y ) ) )
9		iman	|- ( ( x e. A -> x e. y ) <-> -. ( x e. A /\ -. x e. y ) )
10	2	anbi2i	|- ( ( x e. A /\ ph ) <-> ( x e. A /\ -. x e. y ) )
11	9 10	xchbinxr	|- ( ( x e. A -> x e. y ) <-> -. ( x e. A /\ ph ) )
12	8 11	bitrdi	|- ( x e. A -> ( x e. y <-> -. ( x e. A /\ ph ) ) )
13		xor3	|- ( -. ( x e. y <-> ( x e. A /\ ph ) ) <-> ( x e. y <-> -. ( x e. A /\ ph ) ) )
14	12 13	sylibr	|- ( x e. A -> -. ( x e. y <-> ( x e. A /\ ph ) ) )
15	7 14	eximii	|- E. x -. ( x e. y <-> ( x e. A /\ ph ) )
16		exnal	|- ( E. x -. ( x e. y <-> ( x e. A /\ ph ) ) <-> -. A. x ( x e. y <-> ( x e. A /\ ph ) ) )
17	15 16	mpbi	|- -. A. x ( x e. y <-> ( x e. A /\ ph ) )
18	17	nex	|- -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) )