Theorem mobii 2092

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

Syntax hints:   <-> wb 105   T. wtru 1374   E*wmo 2056

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-eu 2058  df-mo 2059

This theorem is referenced by:  moaneu  2132  moanmo  2133  2moswapdc  2146  2exeu  2148  rmobiia  2699  rmov  2797  euxfr2dc  2965  rmoan  2980  2rmorex  2986  mosn  3679  dffun9  5319  funopab  5325  funco  5330  funcnv2  5353  funcnv  5354  fun2cnv  5357  fncnv  5359  imadif  5373  fnres  5412  ovi3  6106  oprabex3  6237  axaddf  8016  axmulf  8017  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  fsum3  11813