Theorem mobii 2123

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

Syntax hints:   <-> wb 105   T. wtru 1403   E*wmo 2087

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-eu 2089  df-mo 2090

This theorem is referenced by:  moaneu  2163  moanmo  2164  2moswapdc  2177  2exeu  2179  rmobiia  2743  rmov  2842  euxfr2dc  3011  rmoan  3026  2rmorex  3032  mosn  3741  dffun9  5401  funopab  5407  funco  5412  funcnv2  5436  funcnv  5437  fun2cnv  5440  fncnv  5442  imadif  5456  fnres  5495  ovi3  6216  oprabex3  6352  axaddf  8225  axmulf  8226  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  fsum3  12132