Theorem mobii 1978

Description: Formula-building rule for "at most one" quantifier (inference rule). (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 1977	. 2 |- ( T. -> ( E* x ps <-> E* x ch ) )
4	3	trud 1293	1 |- ( E* x ps <-> E* x ch )

Syntax hints:   <-> wb 103   T. wtru 1285   E*wmo 1942

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-eu 1944  df-mo 1945

This theorem is referenced by:  moaneu  2017  moanmo  2018  2moswapdc  2031  2exeu  2033  rmobiia  2543  rmov  2619  euxfr2dc  2777  rmoan  2790  2rmorex  2796  mosn  3429  dffun9  4950  funopab  4955  funco  4960  funcnv2  4979  funcnv  4980  fun2cnv  4983  fncnv  4985  imadif  4999  fnres  5035  ovi3  5657  oprabex3  5776  frecuzrdgfn  9414