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  3659  dffun9  5288  funopab  5294  funco  5299  funcnv2  5319  funcnv  5320  fun2cnv  5323  fncnv  5325  imadif  5339  fnres  5377  ovi3  6064  oprabex3  6195  axaddf  7952  axmulf  7953  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  fsum3  11569