Metamath Proof Explorer

Theorem ralnralall

Description: A contradiction concerning restricted generalization for a nonempty set implies anything. (Contributed by Alexander van der Vekens, 4-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. x e. A ( ph /\ -. ph ) <-> ( A. x e. A ph /\ A. x e. A -. ph ) )
2 pm3.24 
 |-  -. ( ph /\ -. ph )
3 2 bifal 
 |-  ( ( ph /\ -. ph ) <-> F. )
4 3 ralbii 
 |-  ( A. x e. A ( ph /\ -. ph ) <-> A. x e. A F. )
5 r19.3rzv 
 |-  ( A =/= (/) -> ( F. <-> A. x e. A F. ) )
6 falim 
 |-  ( F. -> ps )
7 5 6 syl6bir 
 |-  ( A =/= (/) -> ( A. x e. A F. -> ps ) )
8 4 7 syl5bi 
 |-  ( A =/= (/) -> ( A. x e. A ( ph /\ -. ph ) -> ps ) )
9 1 8 syl5bir 
 |-  ( A =/= (/) -> ( ( A. x e. A ph /\ A. x e. A -. ph ) -> ps ) )