Theorem mobii 2079

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 2078	. 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 2043

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-eu 2045  df-mo 2046

This theorem is referenced by:  moaneu  2118  moanmo  2119  2moswapdc  2132  2exeu  2134  rmobiia  2684  rmov  2780  euxfr2dc  2946  rmoan  2961  2rmorex  2967  mosn  3655  dffun9  5284  funopab  5290  funco  5295  funcnv2  5315  funcnv  5316  fun2cnv  5319  fncnv  5321  imadif  5335  fnres  5371  ovi3  6057  oprabex3  6183  axaddf  7930  axmulf  7931  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  fsum3  11533