Metamath Proof Explorer

Theorem mosub

Description: "At most one" remains true after substitution. (Contributed by NM, 9-Mar-1995)

Ref Expression
Hypothesis mosub.1 
|- E* x ph
Assertion mosub 
|- E* x E. y ( y = A /\ ph )

Proof

Step Hyp Ref Expression
1 mosub.1 
 |-  E* x ph
2 moeq 
 |-  E* y y = A
3 1 ax-gen 
 |-  A. y E* x ph
4 moexexvw 
 |-  ( ( E* y y = A /\ A. y E* x ph ) -> E* x E. y ( y = A /\ ph ) )
5 2 3 4 mp2an 
 |-  E* x E. y ( y = A /\ ph )