This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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)

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

Proof

Step Hyp Ref Expression
1 ralf0.1 
 |-  -. ph
2 mtt 
 |-  ( -. ph -> ( -. x e. A <-> ( x e. A -> ph ) ) )
3 1 2 ax-mp 
 |-  ( -. x e. A <-> ( x e. A -> ph ) )
4 3 albii 
 |-  ( A. x -. x e. A <-> A. x ( x e. A -> ph ) )
5 eq0 
 |-  ( A = (/) <-> A. x -. x e. A )
6 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
7 4 5 6 3bitr4ri 
 |-  ( A. x e. A ph <-> A = (/) )