Theorem mobii 2493

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 11	. . 3 |- ( T. -> ( ps <-> ch ) )
3	2	mobidv 2491	. 2 |- ( T. -> ( E* x ps <-> E* x ch ) )
4	3	trud 1493	1 |- ( E* x ps <-> E* x ch )

Syntax hints:   <-> wb 196   T. wtru 1484   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-tru 1486  df-ex 1705  df-nf 1710  df-eu 2474  df-mo 2475

This theorem is referenced by:  moanmo  2532  2moswap  2547  rmobiia  3132  rmov  3222  euxfr2  3391  rmoan  3406  2reu5lem2  3414  reuxfr2d  4891  dffun9  5917  funopab  5923  funcnv2  5957  funcnv  5958  fun2cnv  5960  fncnv  5962  imadif  5973  fnres  6007  ov3  6797  oprabex3  7157  brdom6disj  9354  grothprim  9656  axaddf  9966  axmulf  9967  reuxfr3d  29329  funcnvmptOLD  29467  funcnvmpt  29468  alrmomo  34123  2rmoswap  41184