Theorem r19.32

Description: Theorem 19.32 of Margaris p. 90 with restricted quantifiers, analogous to r19.32v . (Contributed by Alexander van der Vekens, 29-Jun-2017)

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

Proof

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