Theorem mobii 2037

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

Syntax hints:   <-> wb 104   T. wtru 1333   E*wmo 2001

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-eu 2003  df-mo 2004

This theorem is referenced by:  moaneu  2076  moanmo  2077  2moswapdc  2090  2exeu  2092  rmobiia  2623  rmov  2709  euxfr2dc  2873  rmoan  2888  2rmorex  2894  mosn  3567  dffun9  5160  funopab  5166  funco  5171  funcnv2  5191  funcnv  5192  fun2cnv  5195  fncnv  5197  imadif  5211  fnres  5247  ovi3  5915  oprabex3  6035  axaddf  7700  axmulf  7701  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  fsum3  11188