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	$$⊢Ⅎx\phi$$
Assertion	r19.32	$$⊢\forall x\in A\left(\phi \vee \psi \right)\leftrightarrow \left(\phi \vee \forall x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.32.1	$$⊢Ⅎx\phi$$
2	1	nfn	$$⊢Ⅎx\neg \phi$$
3	2	r19.21	$$⊢\forall x\in A\left(\neg \phi \to \psi \right)\leftrightarrow \left(\neg \phi \to \forall x\in A\psi \right)$$
4		df-or	$$⊢\left(\phi \vee \psi \right)\leftrightarrow \left(\neg \phi \to \psi \right)$$
5	4	ralbii	$$⊢\forall x\in A\left(\phi \vee \psi \right)\leftrightarrow \forall x\in A\left(\neg \phi \to \psi \right)$$
6		df-or	$$⊢\left(\phi \vee \forall x\in A\psi \right)\leftrightarrow \left(\neg \phi \to \forall x\in A\psi \right)$$
7	3 5 6	3bitr4i	$$⊢\forall x\in A\left(\phi \vee \psi \right)\leftrightarrow \left(\phi \vee \forall x\in A\psi \right)$$