MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mobii Structured version   Unicode version

Theorem mobii 2301
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
StepHypRef Expression
1 mobii.1 . . . 4  |-  ( ps  <->  ch )
21a1i 11 . . 3  |-  ( T. 
->  ( ps  <->  ch )
)
32mobidv 2299 . 2  |-  ( T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1388 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1380   E*wmo 2276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-tru 1382  df-ex 1597  df-nf 1600  df-eu 2279  df-mo 2280
This theorem is referenced by:  moanmo  2357  moaneuOLD  2359  2moswap  2378  2eu1OLD  2387  rmobiia  3052  rmov  3130  euxfr2  3288  rmoan  3302  2reu5lem2  3310  reuxfr2d  4670  dffun9  5614  funopab  5619  funcnv2  5645  funcnv  5646  fun2cnv  5648  fncnv  5650  imadif  5661  fnres  5695  ov3  6421  oprabex3  6770  brdom6disj  8906  grothprim  9208  axaddf  9518  axmulf  9519  reuxfr3d  27064  funcnvmptOLD  27181  funcnvmpt  27182  2rmoswap  31656
  Copyright terms: Public domain W3C validator