Metamath Proof Explorer

Theorem eubiOLD

Description: Obsolete proof of eubi as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion eubiOLD 
|- ( A. x ( ph <-> ps ) -> ( E! x ph <-> E! x ps ) )

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x ( ph <-> ps )
2 sp 
 |-  ( A. x ( ph <-> ps ) -> ( ph <-> ps ) )
3 1 2 eubid 
 |-  ( A. x ( ph <-> ps ) -> ( E! x ph <-> E! x ps ) )