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

Metamath Proof Explorer

Theorem falseral0

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

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

Proof

Step Hyp Ref Expression
1 alral 
 |-  ( A. x -. ph -> A. x e. A -. ph )
2 pm2.21 
 |-  ( -. ph -> ( ph -> F. ) )
3 2 ral2imi 
 |-  ( A. x e. A -. ph -> ( A. x e. A ph -> A. x e. A F. ) )
4 3 imp 
 |-  ( ( A. x e. A -. ph /\ A. x e. A ph ) -> A. x e. A F. )
5 1 4 sylan 
 |-  ( ( A. x -. ph /\ A. x e. A ph ) -> A. x e. A F. )
6 fal 
 |-  -. F.
7 6 ralf0 
 |-  ( A. x e. A F. <-> A = (/) )
8 5 7 sylib 
 |-  ( ( A. x -. ph /\ A. x e. A ph ) -> A = (/) )