Theorem ralf0

Description: The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005) (Proof shortened by JJ, 14-Jul-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)

	Ref	Expression
Hypothesis	ralf0.1	|- -. ph
Assertion	ralf0	|- ( A. x e. A ph <-> A = (/) )

Proof

Step	Hyp	Ref	Expression
1		ralf0.1	|- -. ph
2		r19.26	|- ( A. x e. A ( -. ph /\ ph ) <-> ( A. x e. A -. ph /\ A. x e. A ph ) )
3		pm2.24	|- ( ph -> ( -. ph -> F. ) )
4	3	impcom	|- ( ( -. ph /\ ph ) -> F. )
5	4	ralimi	|- ( A. x e. A ( -. ph /\ ph ) -> A. x e. A F. )
6		df-ral	|- ( A. x e. A F. <-> A. x ( x e. A -> F. ) )
7		dfnot	|- ( -. x e. A <-> ( x e. A -> F. ) )
8	7	bicomi	|- ( ( x e. A -> F. ) <-> -. x e. A )
9	8	albii	|- ( A. x ( x e. A -> F. ) <-> A. x -. x e. A )
10	6 9	sylbb	|- ( A. x e. A F. -> A. x -. x e. A )
11		id	|- ( x e. A -> x e. A )
12		falim	|- ( F. -> x e. A )
13	11 12	pm5.21ni	|- ( -. x e. A -> ( x e. A <-> F. ) )
14		df-clab	|- ( x e. { y | F. } <-> [ x / y ] F. )
15		sbv	|- ( [ x / y ] F. <-> F. )
16	14 15	bitri	|- ( x e. { y | F. } <-> F. )
17	13 16	bitr4di	|- ( -. x e. A -> ( x e. A <-> x e. { y | F. } ) )
18	17	alimi	|- ( A. x -. x e. A -> A. x ( x e. A <-> x e. { y | F. } ) )
19		dfcleq	|- ( A = { y | F. } <-> A. x ( x e. A <-> x e. { y | F. } ) )
20	18 19	sylibr	|- ( A. x -. x e. A -> A = { y | F. } )
21		dfnul4	|- (/) = { y | F. }
22	20 21	eqtr4di	|- ( A. x -. x e. A -> A = (/) )
23	5 10 22	3syl	|- ( A. x e. A ( -. ph /\ ph ) -> A = (/) )
24	2 23	sylbir	|- ( ( A. x e. A -. ph /\ A. x e. A ph ) -> A = (/) )
25	24	ex	|- ( A. x e. A -. ph -> ( A. x e. A ph -> A = (/) ) )
26	1	a1i	|- ( x e. A -> -. ph )
27	25 26	mprg	|- ( A. x e. A ph -> A = (/) )
28		rzal	|- ( A = (/) -> A. x e. A ph )
29	27 28	impbii	|- ( A. x e. A ph <-> A = (/) )