Theorem falseral0

Description: A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020)

	Ref	Expression
Assertion	falseral0	|- ( ( A. x -. ph /\ A. x e. A ph ) -> A = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		19.26	|- ( A. x ( -. ph /\ ( x e. A -> ph ) ) <-> ( A. x -. ph /\ A. x ( x e. A -> ph ) ) )
3		con3	|- ( ( x e. A -> ph ) -> ( -. ph -> -. x e. A ) )
4	3	impcom	|- ( ( -. ph /\ ( x e. A -> ph ) ) -> -. x e. A )
5	4	alimi	|- ( A. x ( -. ph /\ ( x e. A -> ph ) ) -> A. x -. x e. A )
6		alnex	|- ( A. x -. x e. A <-> -. E. x x e. A )
7	5 6	sylib	|- ( A. x ( -. ph /\ ( x e. A -> ph ) ) -> -. E. x x e. A )
8		notnotb	|- ( A = (/) <-> -. -. A = (/) )
9		neq0	|- ( -. A = (/) <-> E. x x e. A )
10	8 9	xchbinx	|- ( A = (/) <-> -. E. x x e. A )
11	7 10	sylibr	|- ( A. x ( -. ph /\ ( x e. A -> ph ) ) -> A = (/) )
12	2 11	sylbir	|- ( ( A. x -. ph /\ A. x ( x e. A -> ph ) ) -> A = (/) )
13	1 12	sylan2b	|- ( ( A. x -. ph /\ A. x e. A ph ) -> A = (/) )