Theorem mobii 2115

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

Syntax hints:   <-> wb 105   T. wtru 1398   E*wmo 2079

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-eu 2081  df-mo 2082

This theorem is referenced by:  moaneu  2155  moanmo  2156  2moswapdc  2169  2exeu  2171  rmobiia  2723  rmov  2822  euxfr2dc  2990  rmoan  3005  2rmorex  3011  mosn  3704  dffun9  5354  funopab  5360  funco  5365  funcnv2  5389  funcnv  5390  fun2cnv  5393  fncnv  5395  imadif  5409  fnres  5448  ovi3  6161  oprabex3  6293  axaddf  8090  axmulf  8091  frecuzrdgtcl  10677  frecuzrdgfunlem  10684  fsum3  11968