Theorem mobii 2036

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

Syntax hints:   <-> wb 104   T. wtru 1332   E*wmo 2000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-eu 2002  df-mo 2003

This theorem is referenced by:  moaneu  2075  moanmo  2076  2moswapdc  2089  2exeu  2091  rmobiia  2620  rmov  2706  euxfr2dc  2869  rmoan  2884  2rmorex  2890  mosn  3560  dffun9  5152  funopab  5158  funco  5163  funcnv2  5183  funcnv  5184  fun2cnv  5187  fncnv  5189  imadif  5203  fnres  5239  ovi3  5907  oprabex3  6027  axaddf  7676  axmulf  7677  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  fsum3  11156