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	|- ( 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	1	biimpi	|- ( A. x e. A ( ph -> ps ) -> ( ph -> A. x e. A ps ) )