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  5406  funopab  5412  funco  5417  funcnv2  5441  funcnv  5442  fun2cnv  5445  fncnv  5447  imadif  5461  fnres  5500  ovi3  6226  oprabex3  6362  axaddf  8235  axmulf  8236  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  fsum3  12154