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  2802  rmov  2876  euxfr2  3022  rmoan  3035  2reu5lem2  3043  dffun9  5136  funopab  5140  funsn  5148  funcnv2  5156  funcnv  5157  fncnv  5159  imadif  5172  fnres  5200  ov3  5600