Theorem ralinexa

Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005)

	Ref	Expression
Assertion	ralinexa	|- ( A. x e. A ( ph -> -. ps ) <-> -. E. x e. A ( ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		imnan	|- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )
2	1	ralbii	|- ( A. x e. A ( ph -> -. ps ) <-> A. x e. A -. ( ph /\ ps ) )
3		ralnex	|- ( A. x e. A -. ( ph /\ ps ) <-> -. E. x e. A ( ph /\ ps ) )
4	2 3	bitri	|- ( A. x e. A ( ph -> -. ps ) <-> -. E. x e. A ( ph /\ ps ) )