Theorem mobii 2082

Description: Formula-building rule for "at most one" quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
mobii.1	|- ( ps <-> ch )

Assertion

Ref	Expression
mobii	|- ( E* x ps <-> E* x ch )

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		mobii.1	. . . 4 |- ( ps <-> ch )
2	1	a1i 9	. . 3 |- ( T. -> ( ps <-> ch ) )
3	2	mobidv 2081	. 2 |- ( T. -> ( E* x ps <-> E* x ch ) )
4	3	mptru 1373	1 |- ( E* x ps <-> E* x ch )

Syntax hints:   <-> wb 105   T. wtru 1365   E*wmo 2046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-eu 2048  df-mo 2049

This theorem is referenced by:  moaneu  2121  moanmo  2122  2moswapdc  2135  2exeu  2137  rmobiia  2687  rmov  2783  euxfr2dc  2949  rmoan  2964  2rmorex  2970  mosn  3658  dffun9  5287  funopab  5293  funco  5298  funcnv2  5318  funcnv  5319  fun2cnv  5322  fncnv  5324  imadif  5338  fnres  5374  ovi3  6060  oprabex3  6186  axaddf  7935  axmulf  7936  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  fsum3  11552