Theorem mobii 2240

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*xps <-> E*xch)

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		mobii.1	. . . 4 |- (ps <-> ch)
2	1	a1i 10	. . 3 |- ( T. -> (ps <-> ch))
3	2	mobidv 2239	. 2 |- ( T. -> (E*xps <-> E*xch))
4	3	trud 1323	1 |- (E*xps <-> E*xch)

Syntax hints:   <-> wb 176   T. wtru 1316  E*wmo 2205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-tru 1319  df-ex 1542  df-nf 1545  df-eu 2208  df-mo 2209

This theorem is referenced by:  moaneu  2263  moanmo  2264  2moswap  2279  2eu1  2284  rmobiia  2801  rmov  2875  euxfr2  3021  rmoan  3034  2reu5lem2  3042  dffun9  5135  funopab  5139  funsn  5147  funcnv2  5155  funcnv  5156  fncnv  5158  imadif  5171  fnres  5199  ov3  5599