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	biimtrrdi	|- ( A =/= (/) -> ( A. x e. A F. -> ps ) )
8	4 7	biimtrid	|- ( A =/= (/) -> ( A. x e. A ( ph /\ -. ph ) -> ps ) )
9	1 8	biimtrrid	|- ( A =/= (/) -> ( ( A. x e. A ph /\ A. x e. A -. ph ) -> ps ) )