Theorem eubiiOLD

Description: Obsolete version of eubii as of 27-Sep-2023. (Contributed by NM, 9-Jul-1994) (Revised by Mario Carneiro, 6-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	eubii.1	|- ( ph <-> ps )
Assertion	eubiiOLD	|- ( E! x ph <-> E! x ps )

Proof

Step	Hyp	Ref	Expression
1		eubii.1	|- ( ph <-> ps )
2		eubi	|- ( A. x ( ph <-> ps ) -> ( E! x ph <-> E! x ps ) )
3	2 1	mpg	|- ( E! x ph <-> E! x ps )