Theorem r19.32v

Description: Restricted quantifier version of 19.32v . (Contributed by NM, 25-Nov-2003)

	Ref	Expression
Assertion	r19.32v	|- ( A. x e. A ( ph \/ ps ) <-> ( ph \/ A. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		r19.21v	|- ( A. x e. A ( -. ph -> ps ) <-> ( -. ph -> A. x e. A ps ) )
2		df-or	|- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
3	2	ralbii	|- ( A. x e. A ( ph \/ ps ) <-> A. x e. A ( -. ph -> ps ) )
4		df-or	|- ( ( ph \/ A. x e. A ps ) <-> ( -. ph -> A. x e. A ps ) )
5	1 3 4	3bitr4i	|- ( A. x e. A ( ph \/ ps ) <-> ( ph \/ A. x e. A ps ) )