Theorem mosubop

Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995)

	Ref	Expression
Hypothesis	mosubop.1	|- E* x ph
Assertion	mosubop	|- E* x E. y E. z ( A = <. y , z >. /\ ph )

Proof

Step	Hyp	Ref	Expression
1		mosubop.1	|- E* x ph
2	1	gen2	|- A. y A. z E* x ph
3		mosubopt	|- ( A. y A. z E* x ph -> E* x E. y E. z ( A = <. y , z >. /\ ph ) )
4	2 3	ax-mp	|- E* x E. y E. z ( A = <. y , z >. /\ ph )