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

Theorem mobii 2290
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 2288 . 2  |-  ( T. 
->  ( E* x ps  <->  E* x ch ) )
43trud 1447 1  |-  ( E* x ps  <->  E* x ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188   T. wtru 1439   E*wmo 2267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-12 1906
This theorem depends on definitions:  df-bi 189  df-tru 1441  df-ex 1661  df-nf 1665  df-eu 2270  df-mo 2271
This theorem is referenced by:  moanmo  2329  2moswap  2344  2eu1OLD  2352  rmobiia  3020  rmov  3099  euxfr2  3257  rmoan  3271  2reu5lem2  3279  reuxfr2d  4642  dffun9  5627  funopab  5632  funcnv2  5658  funcnv  5659  fun2cnv  5661  fncnv  5663  imadif  5674  fnres  5708  ov3  6445  oprabex3  6794  brdom6disj  8962  grothprim  9261  axaddf  9571  axmulf  9572  reuxfr3d  28117  funcnvmptOLD  28266  funcnvmpt  28267  2rmoswap  38324
  Copyright terms: Public domain W3C validator