Theorem eqab2

Description: Implication of a class abstraction. (Contributed by Peter Mazsa, 16-Apr-2019)

	Ref	Expression
Assertion	eqab2	|- ( A. x ( x e. A <-> ph ) -> A. x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		biimp	|- ( ( x e. A <-> ph ) -> ( x e. A -> ph ) )
2	1	alimi	|- ( A. x ( x e. A <-> ph ) -> A. x ( x e. A -> ph ) )
3		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
4	2 3	sylibr	|- ( A. x ( x e. A <-> ph ) -> A. x e. A ph )