Theorem expandral

Description: Expand a restricted universal quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypothesis	expandral.1	|- ( ph <-> ps )
Assertion	expandral	|- ( A. x e. A ph <-> A. x ( x e. A -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		expandral.1	|- ( ph <-> ps )
2	1	ralbii	|- ( A. x e. A ph <-> A. x e. A ps )
3		df-ral	|- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
4	2 3	bitri	|- ( A. x e. A ph <-> A. x ( x e. A -> ps ) )