This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The empty set 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 )