Theorem ra4v

Description: Version of ra4 with a disjoint variable condition, requiring fewer axioms. This is stdpc5v for a restricted domain. (Contributed by BJ, 27-Mar-2020)

	Ref	Expression
Assertion	ra4v	$$⊢\forall x\in A\left(\phi \to \psi \right)\to \left(\phi \to \forall x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.21v	$$⊢\forall x\in A\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \forall x\in A\psi \right)$$
2	1	biimpi	$$⊢\forall x\in A\left(\phi \to \psi \right)\to \left(\phi \to \forall x\in A\psi \right)$$