Theorem mobii 2051

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 2050	. 2 |- ( T. -> ( E* x ps <-> E* x ch ) )
4	3	mptru 1352	1 |- ( E* x ps <-> E* x ch )

Syntax hints:   <-> wb 104   T. wtru 1344   E*wmo 2015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-eu 2017  df-mo 2018

This theorem is referenced by:  moaneu  2090  moanmo  2091  2moswapdc  2104  2exeu  2106  rmobiia  2655  rmov  2746  euxfr2dc  2911  rmoan  2926  2rmorex  2932  mosn  3612  dffun9  5217  funopab  5223  funco  5228  funcnv2  5248  funcnv  5249  fun2cnv  5252  fncnv  5254  imadif  5268  fnres  5304  ovi3  5978  oprabex3  6097  axaddf  7809  axmulf  7810  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  fsum3  11328