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 )

This proof depends on syntax axioms:   <-> wb 105   T. wtru 1403   E*wmo 2087

This proof depends on 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 proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-eu 2089  df-mo 2090

This theorem is used by:  moaneu  2163  moanmo  2164  2moswapdc  2177  2exeu  2179  rmobiia  2743  rmov  2842  euxfr2dc  3011  rmoan  3026  2rmorex  3032  mosn  3745  dffun9  5409  funopab  5415  funco  5420  funcnv2  5444  funcnv  5445  fun2cnv  5448  fncnv  5450  imadif  5464  fnres  5503  ovi3  6229  oprabex3  6366  axaddf  8241  axmulf  8242  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  fsum3  12179