Theorem rzal

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid df-clel , ax-8 . (Revised by GG, 2-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.21	|- ( -. x e. A -> ( x e. A -> ph ) )
2	1	alimi	|- ( A. x -. x e. A -> A. x ( x e. A -> ph ) )
3		eq0	|- ( A = (/) <-> A. x -. x e. A )
4		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
5	2 3 4	3imtr4i	|- ( A = (/) -> A. x e. A ph )